8 Apr 2013 21:12

## %==%, :==: 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
```_______________________________________________
```
8 Apr 2013 21:59

### 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
```
8 Apr 2013 22:10

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

On Mon, Apr 8, 2013 at 9:59 PM, Richard Eisenberg 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

```_______________________________________________