pyret-lang icon indicating copy to clipboard operation
pyret-lang copied to clipboard

cannot use REPL after putting refinements (aka predicate annotations) on type declarations

Open pnkfelix opened this issue 3 years ago • 2 comments

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://"

pnkfelix avatar Oct 09 '22 21:10 pnkfelix

or actually, maybe this is an instance of a more general problem with type declarations? See e.g. #1623

pnkfelix avatar Oct 10 '22 02:10 pnkfelix

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.

asolove avatar Jan 01 '23 04:01 asolove