Gradual-Typing
Inconsistent `gvector-set!` Behavior under Type-based-casts vs. Coercions
I was trying to come up with an example where erasing casts could lead to value representation issues, and accidentally found what seems to be a bug:
(let ([vec : (GVect Dyn) (gvector 1 #f)])
(begin (print-int 7)
(gvector-set! vec 0 42)
(print-int 9)))
When compiling with --type-based-casts, this code compiles successfully, and prints 7, but never prints 9, and doesn't print any errors. On the other hand, when compiling with --coercions, this prints "7Implicit cast in binding on expression at example.grift:1:25" (which is the cast from (GVect Bool) to (GVect Dyn)).
First, this is clearly inconsistent behavior. Second, I am not sure why when using the coercion representation of casts, this even gives a cast error. Since the vector is parameterized by Dyn, shouldn't we be able to assign anything to it?
I saw other issues where type-based casts exhibit inconsistent behavior. I would be interested in fixing these inconsistencies, although I would like some guidance on what parts of code I should look at. This clearly happens after reduce-to-cast-calculus step, but I'm unsure where to look next.
The type based casts implementation is a bug.
The coercion is not a bug, but is unintuitive. You are starting with a Bool vector casting to a Dynamic vector and then inserting an Int. Since the underlying vector is a bool vector that cast is failing. This cast failing is indicated by the source position in the cast failure message. If you want a truly dynamic vector which can store both Ints and Bools then you want the underlying representation to be a dynamic vector. To get one, you will need to initialize the vector with a dynamically typed value. For instance (gvector 1 (#t : Dyn)). Hope it helps.
I will try to locate some places in the code you might start looking, also I am trying to finish a rough draft of my thesis chapter that describes grift. I will try to get back with you this weekend. If I don't please ping me.
On Thu, Apr 15, 2021, 1:27 PM Temur Saidkhodjaev @.***> wrote:
I was trying to come up with an example where erasing casts could lead to value representation issues, and accidentally found what seems to be a bug:
(let ([vec : (GVect Dyn) (gvector 1 #f)]) (begin (print-int 7) (gvector-set! vec 0 42) (print-int 9)))
When compiling with --type-based-casts, this code compiles successfully, and prints 7, but never prints 9, and doesn't print any errors. On the other hand, when compiling with --coercions, this prints "7Implicit cast in binding on expression at example.grift:1:25" (which is the cast from (GVect Bool) to (GVect Dyn)). First, this is clearly inconsistent behavior. Second, I am not sure why when using the coercion representation of casts, this even gives a cast error. Since the vector is parameterized by Dyn, shouldn't we be able to assign anything to it? I saw other issues where type-based casts exhibit inconsistent behavior. I would be interested in fixing these inconsistencies, although I would like some guidance on what parts of code I should look at. This clearly happens after reduce-to-cast-calculus step, but I'm unsure where to look next.
— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/Gradual-Typing/Grift/issues/115, or unsubscribe https://github.com/notifications/unsubscribe-auth/ABBMUMQE2EWETXAWIR2WZELTI5D3JANCNFSM43AGIGYA .
