[Haskell-cafe] %==%, :==: and type equality in the singletons library

Paul Brauner polux2001 at gmail.com
Mon Apr 8 22:10:08 CEST 2013

On Mon, Apr 8, 2013 at 9:59 PM, Richard Eisenberg <eir at cis.upenn.edu> wrote:

> On Apr 8, 2013, at 3:12 PM, Paul Brauner <polux2001 at gmail.com> wrote:
> > from the output of -ddump-splices I dont think it is the case but I'm
> asking anyway: is there any way to deduce a ~ b from a :==: b?
> Not easily. You would have to write a (potentially recursive) function
> that explicitly matches singleton constructors, similarly to what you
> wrote. (You could say that this function is a (potentially inductive) proof
> that the generated definition of :==: is correct.)


> I agree that this is boilerplate and could easily be generated. I've added
> it to the list of features to be included in the next version of
> singletons. I'm surprised myself that it hasn't occurred to me to include
> this before.


>  Richard
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20130408/ebd68eec/attachment.htm>

More information about the Haskell-Cafe mailing list