4 ms·
There is an easy design choice - which Haskell didn't take - which would allow us to have transparent Identity functors, associative Compose and many others: Ad
by fmap 9y ago
There is an easy design choice - which Haskell didn't take - which would allow us to have transparent Identity functors, associative Compose and many others: Add a conversion rule to your language and don't eagerly expand definitions at the type level.
For example, in Coq you would write
Definition Identity a := a.
Definition Compose F G a := F (G a).
Instance: Functor Identity. Proof[...]
and so on. This works, since explicit conversion during type checking allows you to associate type classes to otherwise transparent definitions.
Of course, this is no silver bullet and complicates other things. Everything works out beautifully though, if you combine conversion with bidirectional type checking, at the expense of less powerful type inference.
- hyperpape 9y agoInterestingly, the author did a dissertation using Coq, so I wonder if he thinks that it's not really suitable.
- fmap 9y agoI don't know, but Russel O'Connor got his PhD in 2008, the same year that type classes were introduced in Coq. There has been a lot of development on the Coq proof assistant since then. I don't imagine that working with Coq in 2008 was particularly pleasant. :)
- auggierose 9y agoI don't think working with Coq has ever or will ever be particularly pleasant :-) O'Connor gave a nice talk at TPHol's which I attended: https://arxiv.org/abs/cs/0505034 https://arxiv.org/abs/cs/0505034 Keeping up with Coq shouldn't have been too difficult for him.
- lmm 9y agoWhat does Idris do? That seems to be the best hope of combining Coq-like advanced typing with Haskell-like practicality.