This is my main gripe with Agda, the culture, design decisions and certain syntax forces you into applied style
Conversation
Nothing in Agda forces you to use a pi type instead of ->. It's not even considered idiomatic to do that.
1
1
That's not what I'm saying, agda writes
data Maybe (a : Set l) : Set l where
instead of
data Maybe : Set l -> Set l ..
3
The difference is whether it is an 'index' or a 'parameter'. Indexes can vary between constructors, parameters can't. agda.readthedocs.io/en/v2.6.0.1/la - IIRC in some DT langs the difference is significant - either for unification or erasure or something, but not sure for Agda.
1
Haskell doesn't have that distinction and also doesn't force you to quantify type variables which is my ideal syntax!
1
I agree! But Haskell has stratification between types and terms which makes efficient code generation easier. I'm not sure if that's the thing at play here, but smushing together stuff makes things mighty hard. They also have to deal with positivity checking for data types too!
1
Ahh, it seems like using parameters is always preferred because it allows the pattern match elaborator to prune more cases automatically in proofs/definitions: stackoverflow.com/a/24601292
1
1
Not sure if there's any way to infer parameters vs. indices, and it might also be important for documentation/intent. I do agree that the arrow notation looks prettier than the ML-style inline-annotated arguments.
Some more links, this time regarding how indexes vs. parameters affect the generation of induction principles (I don't think this is what Agda does internally, but I believe it's pretty important for the type theory):
cs.stackexchange.com/questions/2010
homotopytypetheory.org/2011/04/10/jus