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
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!
1
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
Replying to
Different symbol is a good idea, but would be more like:
( a · A : Type) -> ..
Allowing the `:` later would just annotate the parameter’s type.
I might have confused things by using the term ‘quantification’ 🤦♂️🤦♂️
Replying to
That's nicer, in honor of reddit.com/r/haskell/comm I will throw using both :: and : into the ring
(n :: Nat : Type) -> (Fin n : Type)
{n :: Nat : Type) -> (Fin n : Type)
syntax is fun