Paul Brauner | 8 Apr 21:12 2013
Picon

%==%, :==: and type equality in the singletons library

Hello,

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? 

Given

  data T = C1 | ... | Cn

I can easily derive

  data EqT :: T -> T -> * where
     EqT :: a ~ b => EqT a b

  eqT :: ST a -> ST b -> Maybe (EqT a b)
  eqT SC1 SC1 = Just EqT
  ...
  eqT SCn SCn = Just EqT
  eqT _ _ = Nothing

but this kind of replicates the boilerplate generated by the singletons library for %==%. However I can't see how to leverage %==% to inhabit eqT since I can't deduce a ~ b from a %==% b == STrue.

Any idea? If there's no way to write eqT using what singletons generates, wouldn't it make sense for it to generate something that relates :==: and ~ ?

Cheers,
Paul
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Richard Eisenberg | 8 Apr 21:59 2013

Re: %==%, :==: and type equality in the singletons library


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
Paul Brauner | 8 Apr 22:10 2013
Picon

Re: %==%, :==: and type equality in the singletons library




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.)

Ok.
 
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.


Great!

Paul
 
Richard



_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Gmane