Conversation

You get annoying ambiguities with the dependent function syntax - ie. `(A : Set) -> A` - is this a non-dependent function from `A -> A` with the first `A` annotated, or is it a dependent function with a parameter named `A`?

I appreciate Haskell more using identifiers to indicate that the left-hand of :: is a quantifiee forall (n :: Nat). .. pi (n :: Nat). .. otherwise, it's an annotation: (Eq a :: Constraint) => .. (Int :: Type) -> ..

(a : A) -> .. {b : B} -> .. beautiful but perhaps too minimal, I have minor experience of Agda though

Brendan Zabarauskas

@brendanzab

I like Agda’s because it makes it clear that universal quantification is just a form of function type, but yeah, can be a right old pain to parse, especially if you want to support infix annotations. Let me know if you have any brilliant ideas!

gulp, the problem is that the same symbol :/:: is used for quantification and type annotation? If so (·) or another sigil can denote quantification ( a · A ) -> .. { a · A } -> .. and (:) annotation ( a · (A : type) : A ) -> .. { a · (A : Type) : A } -> ..

for *dependent* quantification

Brendan Zabarauskas

@brendanzab