Skip to content

Expression type annotation vs. Declaration type annotation #73

Open
@AlexKnauth

Description

@AlexKnauth

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.

  1. 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 is ann, but Hackett might need something different since : is already the expression version.

  2. 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.)

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions