Description
Similar to how :
declarations work in Typed Racket or how id :: type
declarations work in Haskell, I want to be able to separate definitions from their type annotations like this:
(: f {Integer -> Integer})
(def f (λ [x] x))
I have already implemented most of this (same way as Stephen and I did this in Typed Rosette), but there are some design questions left over.
-
The expression form of type annotation is already called
:
, and in places where both definitions and expressions are allowed, calling them both:
would be ambiguous. The expression version and the declaration version should probably have different names. In Typed Racket the declaration version is:
and the expression version isann
, but Hackett might need something different since:
is already the expression version. -
My preliminary implementation of this doesn't include Scoped Type Variables. I have had trouble "communicating" the scope between the type declaration form and the definition form where the scope is needed. We're working on this now. (Edit: now solved.)