Stream: hs-to-coq devs & users

Topic: Representation of Classes

Li-yao (Nov 16 2020 at 17:26):

Why does hs-to-coq CPS transform type class dictionaries?

Record Functor_Dict F := { fmap : ... }.

Class Functor F :=
  fdict : forall R, (Functor_Dict F -> R) -> R.

Stephanie Weirich (Nov 16 2020 at 20:24):

The CPS transform helps Coq see the termination argument for some instances. See the "Recursion through Instances" section of the Total Haskell is Reasonable Coq paper. https://arxiv.org/pdf/1711.09286.pdf

Last updated: Feb 06 2023 at 05:03 UTC