pyret-lang
pyret-lang copied to clipboard
cannot use REPL after putting refinements (aka predicate annotations) on type declarations
Consider the following code:
WIDTH = 3
fun in-bounds(x :: Number) -> Boolean:
(0 <= x) and (x < WIDTH)
end
data PlaceV0: place-d-v0(x :: Number % (in-bounds), y :: Number % (in-bounds)) end
fun place-t-v0(x :: Number % (in-bounds), y :: Number % (in-bounds)) -> {Number % (in-bounds); Number % (in-bounds)}:
{x; y}
end
# type Coord = Number % (in-bounds)
# data Place: place-d-v1(x :: Coord, y :: Coord) end
# fun place-t-v1(x :: Coord, y :: Coord) -> {Coord; Coord}: {x; y} end
It runs, and you can do things like place-d-v0(2, 2) in the REPL, and you get values you expect.
But, as you might have predicted, I wanted to avoid the repeating the refinement annotation, So I tried to make a type, Coord.
As soon as you uncomment type Coord = Number % (in-bounds) above, then the repl complains in response to any interactions , saying:
"Could not find type Coord on module definitions://"
or actually, maybe this is an instance of a more general problem with type declarations? See e.g. #1623
The refined named type works correctly if you switch from untyped to typed run mode in CPO, so I think this is the same as #1677.