3 ms·
"Classes are just records with additional functionality, which makes them into a haskell-style type classes." But (IIUC) without coherence?
by dllthomas 7y ago
"Classes are just records with additional functionality, which makes them into a haskell-style type classes."
But (IIUC) without coherence?
- Blaisorblade0 7y agoGood point, but never seen typeclass coherence with dependent types (in either Coq or the various versions of the Agda design). Not sure for Isabelle.
- dllthomas 7y agoI'm not sure I can name another language with coherence, dependant types or not. To be fair, even GHC is half-hearted about it.