Arend: Theorem Prover Based on Homotopy Type Theory by JetBrains

Re:Arend: Theorem Prover Based on Homotopy Type Theory by Je... by dllthomas on Wednesday August 07, 2019 @01:12PM (#20636715)

"Classes are just records with additional functionality, which makes them into a haskell-style type classes."

But (IIUC) without coherence?

[ Parent | on HN ]

Re:Arend: Theorem Prover Based on Homotopy Type Theory by Je... by Blaisorblade0 on Sunday August 11, 2019 @07:13AM (#20667594)

Good point, but never seen typeclass coherence with dependent types (in either Coq or the various versions of the Agda design). Not sure for Isabelle.

[ Parent | on HN ]

Re:Arend: Theorem Prover Based on Homotopy Type Theory by Je... by dllthomas on Sunday August 11, 2019 @12:55PM (#20669041)

I'm not sure I can name another language with coherence, dependant types or not. To be fair, even GHC is half-hearted about it.

[ Parent | on HN ]