Why on Earth not
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`?
2
1
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) -> ..
1
(a : A) -> ..
{b : B} -> ..
beautiful but perhaps too minimal, I have minor experience of Agda though
1
1
Replying to
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!
Replying to
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 } -> ..
2
1
for *dependent* quantification
2
1
Show replies