>>13025019>betterAgda is dependently typed, Haskell is not. There's no better or worse per se with type systems, just like it's the case with logic theories.
For example, Haskell has type polymorphism, giving universal quantifiers for types but not e.g. type equality checking functions.
With the Haskell compiler cam write the function type
and it will give you the identity function on that type,
and so you don't have to code it yourself.
Similarly, you can give the compiler the function type
and it will tell you that the pair-flip function
is the only fitting function and give you that.
(Under Curry-Howard, those correspond to the law of identity, essentially, as well as the commutivity of conjunction , respectively.)
Now you could think that making the system stronger would make it better - but sadly logical systems are easily robbed features by giving it strength..
So if you for example are able to use types as values and test against them, then
which captures a simple logical law on type level, doesn't have a unique polymorphic solution anymore. Consider this function f:
f(x) returns 9001 if a=Int, else return x
