Why on Earth not
Conversation
Replying to
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`?
1
For now in github.com/brendanzab/rus I've decided to use a keyword to disambiguate it `Fun (A : Type) -> A` - still not super happy though. 😰
Replying to
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
Show replies