TypeLits and type families wrt. equality

Gabor Greif

24 Jul 2015 24 Jul '15

11:01 a.m.

Hi all! I have a problem with following disconnect: equalities for types as detectable by type families, while I am missing a convincing technique to do the same at the value level. (convincing means here: without resorting to unsafeCoerce) Here is a demo snippet illustrating the issue. Try to get the commented line to compile without using unsafeCoerce. ############################################################## {-# LANGUAGE DataKinds, GADTs, TypeOperators , KindSignatures, ScopedTypeVariables, TypeFamilies #-} import Data.Type.Equality import GHC.TypeLits import Data.Proxy data Path (names :: [Symbol]) where Empty :: Path '[] Longer :: KnownSymbol name => Proxy name -> Path names -> Path (name ': names) type family StripOut (name :: Symbol) (path :: [Symbol]) where StripOut name '[] = '[] StripOut name (name ': ns) = StripOut name ns StripOut n (name ': ns) = n ': StripOut name ns stripOut :: KnownSymbol name => Proxy name -> Path names -> Path (StripOut name names) stripOut _ Empty = Empty stripOut n (Longer n' path) | Just Refl <- n `sameSymbol` n' = stripOut n path --stripOut n (Longer n' path) = Longer n' (stripOut n path) ############################################################## I get the error reproduced at the end of this message. My suspicion is that we need to model type inequality (with a new built-in eliminator, perhaps?) that helps us to skip the equation "StripOut name (name ': ns) = StripOut name ns" in the case when sameSymbol would return Nothing. Any ideas? Cheers and thanks Gabor ----------------------------------------------------- Lits.hs:20:31: error: Could not deduce: StripOut name (name1 : names1) ~ (name1 : StripOut name names1) from the context: (names ~ (name1 : names1), KnownSymbol name1) bound by a pattern with constructor: Longer :: forall (name :: Symbol) (names :: [Symbol]). KnownSymbol name => Proxy name -> Path names -> Path (name : names), in an equation for stripOut at Lits.hs:20:13-26 Expected type: Path (StripOut name names) Actual type: Path (name1 : StripOut name names1) Relevant bindings include path :: Path names1 (bound at Lits.hs:20:23) n' :: Proxy name1 (bound at Lits.hs:20:20) n :: Proxy name (bound at Lits.hs:20:10) stripOut :: Proxy name -> Path names -> Path (StripOut name names) (bound at Lits.hs:18:1) In the expression: Longer n' (stripOut n path) In an equation for stripOut : stripOut n (Longer n' path) = Longer n' (stripOut n path) Failed, modules loaded: none.

Show replies by date

Anthony Cowley

24 Jul 24 Jul

12:31 p.m.

I think you are already very familiar with what I'll show here, but I figured I'd offer this alternative approach just in case. It does not directly address your type error, but does show one way of loosely steering values from the type level. https://gist.github.com/acowley/57724b6facd6a39a196f Anthony Gabor Greif writes:

...

Hi all!

I have a problem with following disconnect: equalities for types as detectable by type families, while I am missing a convincing technique to do the same at the value level. (convincing means here: without resorting to unsafeCoerce)

Here is a demo snippet illustrating the issue. Try to get the commented line to compile without using unsafeCoerce.

############################################################## {-# LANGUAGE DataKinds, GADTs, TypeOperators , KindSignatures, ScopedTypeVariables, TypeFamilies #-}

import Data.Type.Equality import GHC.TypeLits import Data.Proxy

data Path (names :: [Symbol]) where Empty :: Path '[] Longer :: KnownSymbol name => Proxy name -> Path names -> Path (name ': names)

type family StripOut (name :: Symbol) (path :: [Symbol]) where StripOut name '[] = '[] StripOut name (name ': ns) = StripOut name ns StripOut n (name ': ns) = n ': StripOut name ns

stripOut :: KnownSymbol name => Proxy name -> Path names -> Path (StripOut name names) stripOut _ Empty = Empty stripOut n (Longer n' path) | Just Refl <- n `sameSymbol` n' = stripOut n path --stripOut n (Longer n' path) = Longer n' (stripOut n path) ##############################################################

I get the error reproduced at the end of this message.

My suspicion is that we need to model type inequality (with a new built-in eliminator, perhaps?) that helps us to skip the equation "StripOut name (name ': ns) = StripOut name ns" in the case when sameSymbol would return Nothing.

Any ideas?

Cheers and thanks

Gabor

-----------------------------------------------------

Lits.hs:20:31: error: Could not deduce: StripOut name (name1 : names1) ~ (name1 : StripOut name names1) from the context: (names ~ (name1 : names1), KnownSymbol name1) bound by a pattern with constructor: Longer :: forall (name :: Symbol) (names :: [Symbol]). KnownSymbol name => Proxy name -> Path names -> Path (name : names), in an equation for stripOut at Lits.hs:20:13-26 Expected type: Path (StripOut name names) Actual type: Path (name1 : StripOut name names1) Relevant bindings include path :: Path names1 (bound at Lits.hs:20:23) n' :: Proxy name1 (bound at Lits.hs:20:20) n :: Proxy name (bound at Lits.hs:20:10) stripOut :: Proxy name -> Path names -> Path (StripOut name names) (bound at Lits.hs:18:1) In the expression: Longer n' (stripOut n path) In an equation for stripOut : stripOut n (Longer n' path) = Longer n' (stripOut n path) Failed, modules loaded: none. _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Gabor Greif

25 Jul 25 Jul

6:08 a.m.

Hi Anthony, while I suspected that one would need to go the "value inference" route (i.e. type classes), I had no idea how to get started. So thanks for your snippet, it is very helpful. Otoh, it only strips one segment ``` haskell *GaborTEq> showPath $ stripOut (Proxy :: Proxy "Hey") (Longer (Proxy :: Proxy "Du") $ Longer (Proxy :: Proxy "Hey") $ Longer (Proxy :: Proxy "Bee") $ Longer (Proxy :: Proxy "Hey") $ Longer (Proxy :: Proxy "Hey") $ Empty) "Du -> Bee -> Hey -> Hey" ``` I'll play around a bit with FDs and see what I can figure out to make this work. Cheers, Gabor On 7/24/15, Anthony Cowley wrote:

...

I think you are already very familiar with what I'll show here, but I figured I'd offer this alternative approach just in case. It does not directly address your type error, but does show one way of loosely steering values from the type level.

https://gist.github.com/acowley/57724b6facd6a39a196f

Anthony

Gabor Greif writes:

...
Hi all!

I have a problem with following disconnect: equalities for types as detectable by type families, while I am missing a convincing technique to do the same at the value level. (convincing means here: without resorting to unsafeCoerce)

Here is a demo snippet illustrating the issue. Try to get the commented line to compile without using unsafeCoerce.

############################################################## {-# LANGUAGE DataKinds, GADTs, TypeOperators , KindSignatures, ScopedTypeVariables, TypeFamilies #-}

import Data.Type.Equality import GHC.TypeLits import Data.Proxy

data Path (names :: [Symbol]) where Empty :: Path '[] Longer :: KnownSymbol name => Proxy name -> Path names -> Path (name ': names)

type family StripOut (name :: Symbol) (path :: [Symbol]) where StripOut name '[] = '[] StripOut name (name ': ns) = StripOut name ns StripOut n (name ': ns) = n ': StripOut name ns

stripOut :: KnownSymbol name => Proxy name -> Path names -> Path (StripOut name names) stripOut _ Empty = Empty stripOut n (Longer n' path) | Just Refl <- n `sameSymbol` n' = stripOut n path --stripOut n (Longer n' path) = Longer n' (stripOut n path) ##############################################################

I get the error reproduced at the end of this message.

My suspicion is that we need to model type inequality (with a new built-in eliminator, perhaps?) that helps us to skip the equation "StripOut name (name ': ns) = StripOut name ns" in the case when sameSymbol would return Nothing.

Any ideas?

Cheers and thanks

Gabor

-----------------------------------------------------

Lits.hs:20:31: error: Could not deduce: StripOut name (name1 : names1) ~ (name1 : StripOut name names1) from the context: (names ~ (name1 : names1), KnownSymbol name1) bound by a pattern with constructor: Longer :: forall (name :: Symbol) (names :: [Symbol]). KnownSymbol name => Proxy name -> Path names -> Path (name : names), in an equation for stripOut at Lits.hs:20:13-26 Expected type: Path (StripOut name names) Actual type: Path (name1 : StripOut name names1) Relevant bindings include path :: Path names1 (bound at Lits.hs:20:23) n' :: Proxy name1 (bound at Lits.hs:20:20) n :: Proxy name (bound at Lits.hs:20:10) stripOut :: Proxy name -> Path names -> Path (StripOut name names) (bound at Lits.hs:18:1) In the expression: Longer n' (stripOut n path) In an equation for stripOut : stripOut n (Longer n' path) = Longer n' (stripOut n path) Failed, modules loaded: none. _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Simon Peyton Jones

27 Jul 27 Jul

9:48 a.m.

Yes. Here's a simpler example: ===================================== type family Equal a b where Equal a a = 'True Equal a b = 'False foo :: Proxy 'True -> Bool foo x = True f :: forall a b. Maybe (a :~: b) -> Bool f x = case x of Just Refl -> True Nothing -> foo (undefined :: Proxy (Equal a b)) ===================================== In the 'Nothing' branch of the case, we know that a is not equal to b; but we don't exploit that negative information when trying to reduce (Equal a b). Making type inference (and system FC) exploit negative info would be a Big Deal, I think. Simon | -----Original Message----- | From: ghc-devs [mailto:ghc-devs-bounces@haskell.org] On Behalf Of | Gabor Greif | Sent: 24 July 2015 16:02 | To: ghc-devs; Richard Eisenberg | Subject: TypeLits and type families wrt. equality | | Hi all! | | I have a problem with following disconnect: equalities for types as | detectable by type families, while I am missing a convincing technique | to do the same at the value level. (convincing means here: without | resorting to unsafeCoerce) | | Here is a demo snippet illustrating the issue. Try to get the | commented line to compile without using unsafeCoerce. | | ############################################################## | {-# LANGUAGE DataKinds, GADTs, TypeOperators | , KindSignatures, ScopedTypeVariables, TypeFamilies #-} | | import Data.Type.Equality | import GHC.TypeLits | import Data.Proxy | | data Path (names :: [Symbol]) where | Empty :: Path '[] | Longer :: KnownSymbol name => Proxy name -> Path names -> Path (name | ': names) | | type family StripOut (name :: Symbol) (path :: [Symbol]) where | StripOut name '[] = '[] | StripOut name (name ': ns) = StripOut name ns | StripOut n (name ': ns) = n ': StripOut name ns | | stripOut :: KnownSymbol name => Proxy name -> Path names -> Path | (StripOut name names) | stripOut _ Empty = Empty | stripOut n (Longer n' path) | Just Refl <- n `sameSymbol` n' = | stripOut n path | --stripOut n (Longer n' path) = Longer n' (stripOut n path) | ############################################################## | | I get the error reproduced at the end of this message. | | My suspicion is that we need to model type inequality (with a new | built-in eliminator, perhaps?) that helps us to skip the equation | "StripOut name (name ': ns) = StripOut name ns" in the case when | sameSymbol would return Nothing. | | Any ideas? | | Cheers and thanks | | Gabor | | | ----------------------------------------------------- | | | Lits.hs:20:31: error: | Could not deduce: StripOut name (name1 : names1) | ~ (name1 : StripOut name names1) | from the context: (names ~ (name1 : names1), KnownSymbol name1) | bound by a pattern with constructor: | Longer :: forall (name :: Symbol) (names :: | [Symbol]). | KnownSymbol name => | Proxy name -> Path names -> Path (name : | names), | in an equation for stripOut | at Lits.hs:20:13-26 | Expected type: Path (StripOut name names) | Actual type: Path (name1 : StripOut name names1) | Relevant bindings include | path :: Path names1 | (bound at Lits.hs:20:23) | n' :: Proxy name1 | (bound at Lits.hs:20:20) | n :: Proxy name | (bound at Lits.hs:20:10) | stripOut :: Proxy name -> Path names -> Path (StripOut name | names) | (bound at Lits.hs:18:1) | In the expression: Longer n' (stripOut n path) | In an equation for stripOut : | stripOut n (Longer n' path) = Longer n' (stripOut n path) | Failed, modules loaded: none. | _______________________________________________ | ghc-devs mailing list | ghc-devs@haskell.org | http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Gabor Greif

10:36 a.m.

Simon, yes, this is the the same problem. You probably meant: ===================================== type family Equal a b where Equal a a = 'True Equal a b = 'False foo :: Proxy 'False -> Bool foo x = False f :: forall a b. Maybe (a :~: b) -> Bool f x = case x of Just Refl -> True Nothing -> foo (undefined :: Proxy (Equal a b)) ===================================== When saying "Big Deal" did you mean - highly desirable and somebody should go for it - or a terrible amount of work, and who tackles it is probably a fool on a hubris trip? (I still have my problems deciphering British irony.) I guess a full-blown solution is too much work for now (also considering previous comments from Richard). But what about a simpler construct decideRefl :: Proxy (a :: Symbol) -> Proxy b -> Proxy (Equal a b :~: 'False) -> Either (Equal a b :~: 'False) (a :~: b) The Right case is just rewrapping the Refl from a `sameSymbol`, while the Left injection would suppress the clause "Equal a a = 'True" from the type family, knowing that it cannot contribute to an outcome, arriving at the 'False result. (I have no idea how this could be represented in Core, though.) What do you think? Cheers, Gabor On 7/27/15, Simon Peyton Jones wrote:

...

Yes. Here's a simpler example:

===================================== type family Equal a b where Equal a a = 'True Equal a b = 'False

foo :: Proxy 'True -> Bool foo x = True

f :: forall a b. Maybe (a :~: b) -> Bool f x = case x of Just Refl -> True Nothing -> foo (undefined :: Proxy (Equal a b)) =====================================

In the 'Nothing' branch of the case, we know that a is not equal to b; but we don't exploit that negative information when trying to reduce (Equal a b).

Making type inference (and system FC) exploit negative info would be a Big Deal, I think.

Simon

| -----Original Message----- | From: ghc-devs [mailto:ghc-devs-bounces@haskell.org] On Behalf Of | Gabor Greif | Sent: 24 July 2015 16:02 | To: ghc-devs; Richard Eisenberg | Subject: TypeLits and type families wrt. equality | | Hi all! | | I have a problem with following disconnect: equalities for types as | detectable by type families, while I am missing a convincing technique | to do the same at the value level. (convincing means here: without | resorting to unsafeCoerce) | | Here is a demo snippet illustrating the issue. Try to get the | commented line to compile without using unsafeCoerce. | | ############################################################## | {-# LANGUAGE DataKinds, GADTs, TypeOperators | , KindSignatures, ScopedTypeVariables, TypeFamilies #-} | | import Data.Type.Equality | import GHC.TypeLits | import Data.Proxy | | data Path (names :: [Symbol]) where | Empty :: Path '[] | Longer :: KnownSymbol name => Proxy name -> Path names -> Path (name | ': names) | | type family StripOut (name :: Symbol) (path :: [Symbol]) where | StripOut name '[] = '[] | StripOut name (name ': ns) = StripOut name ns | StripOut n (name ': ns) = n ': StripOut name ns | | stripOut :: KnownSymbol name => Proxy name -> Path names -> Path | (StripOut name names) | stripOut _ Empty = Empty | stripOut n (Longer n' path) | Just Refl <- n `sameSymbol` n' = | stripOut n path | --stripOut n (Longer n' path) = Longer n' (stripOut n path) | ############################################################## | | I get the error reproduced at the end of this message. | | My suspicion is that we need to model type inequality (with a new | built-in eliminator, perhaps?) that helps us to skip the equation | "StripOut name (name ': ns) = StripOut name ns" in the case when | sameSymbol would return Nothing. | | Any ideas? | | Cheers and thanks | | Gabor | | | ----------------------------------------------------- | | | Lits.hs:20:31: error: | Could not deduce: StripOut name (name1 : names1) | ~ (name1 : StripOut name names1) | from the context: (names ~ (name1 : names1), KnownSymbol name1) | bound by a pattern with constructor: | Longer :: forall (name :: Symbol) (names :: | [Symbol]). | KnownSymbol name => | Proxy name -> Path names -> Path (name : | names), | in an equation for stripOut | at Lits.hs:20:13-26 | Expected type: Path (StripOut name names) | Actual type: Path (name1 : StripOut name names1) | Relevant bindings include | path :: Path names1 | (bound at Lits.hs:20:23) | n' :: Proxy name1 | (bound at Lits.hs:20:20) | n :: Proxy name | (bound at Lits.hs:20:10) | stripOut :: Proxy name -> Path names -> Path (StripOut name | names) | (bound at Lits.hs:18:1) | In the expression: Longer n' (stripOut n path) | In an equation for stripOut : | stripOut n (Longer n' path) = Longer n' (stripOut n path) | Failed, modules loaded: none. | _______________________________________________ | ghc-devs mailing list | ghc-devs@haskell.org | http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Richard Eisenberg

10:44 a.m.

On Jul 27, 2015, at 10:36 AM, Gabor Greif wrote:

...

When saying "Big Deal" did you mean - highly desirable and somebody should go for it - or a terrible amount of work, and who tackles it is probably a fool on a hubris trip?

(I still have my problems deciphering British irony.)

My use of Big Deal here is more your second option, but without so much negativity. :) I'm sure the person who tackled this problem would learn a ton and contribute to programming language research. It's just that we haven't yet found a great motivation for doing so.

...

I guess a full-blown solution is too much work for now (also considering previous comments from Richard). But what about a simpler construct

decideRefl :: Proxy (a :: Symbol) -> Proxy b -> Proxy (Equal a b :~: 'False) -> Either (Equal a b :~: 'False) (a :~: b)

I believe that this function could be written only with the help of unsafeCoerce. Indeed, the `singletons` package provides an `SDecide` instance for the type-lits (which accomplishes a similar, though not identical, goal) via unsafeCoerce. Richard

Gabor Greif

10:56 a.m.

On 7/27/15, Richard Eisenberg wrote:

...

On Jul 27, 2015, at 10:36 AM, Gabor Greif wrote:

...
When saying "Big Deal" did you mean - highly desirable and somebody should go for it - or a terrible amount of work, and who tackles it is probably a fool on a hubris trip?

(I still have my problems deciphering British irony.)

My use of Big Deal here is more your second option, but without so much negativity. :) I'm sure the person who tackled this problem would learn a ton and contribute to programming language research. It's just that we haven't yet found a great motivation for doing so.

Okay, agreed.

...

...
I guess a full-blown solution is too much work for now (also considering previous comments from Richard). But what about a simpler construct

decideRefl :: Proxy (a :: Symbol) -> Proxy b -> Proxy (Equal a b :~: 'False) -> Either (Equal a b :~: 'False) (a :~: b)

I believe that this function could be written only with the help of unsafeCoerce. Indeed, the `singletons` package provides an `SDecide` instance for the type-lits (which accomplishes a similar, though not identical, goal) via unsafeCoerce.

I doubt it could even be written with unsafeCoerce. It would need some magic sauce from the compiler, tapping into the type family normalizer. Consider:

...

decideRefl (Proxy :: Proxy "a") (Proxy :: Proxy "b") (Proxy :: Proxy (Equal a b :~: 'True)

This should give a type error (we shouldn't fabricate false evidence!), while

...

decideRefl (Proxy :: Proxy "a") (Proxy :: Proxy "b") (Proxy :: Proxy (Equal a b :~: 'False)

should pass the type checker and give Left Refl. Cheers, Gabor

...

Richard

Richard Eisenberg

11:08 a.m.

On Jul 27, 2015, at 10:56 AM, Gabor Greif wrote:

...

...
...
decideRefl :: Proxy (a :: Symbol) -> Proxy b -> Proxy (Equal a b :~: 'False) -> Either (Equal a b :~: 'False) (a :~: b)

What's the point of the third Proxy argument? I don't think it adds anything. Perhaps without that the way forward (albeit still with unsafeCoerce) will become clear. Richard

Gabor Greif

11:22 a.m.

On 7/27/15, Richard Eisenberg wrote:

...

On Jul 27, 2015, at 10:56 AM, Gabor Greif wrote:

...
...
...
decideRefl :: Proxy (a :: Symbol) -> Proxy b -> Proxy (Equal a b :~: 'False) -> Either (Equal a b :~: 'False) (a :~: b)

What's the point of the third Proxy argument? I don't think it adds anything. Perhaps without that the way forward (albeit still with unsafeCoerce) will become clear.

Proxy (Equal a b :~: 'False) is just the specialised version to the general issue I'd like to crack: Proxy a -> Proxy b -> Proxy (<some type-level expression mentioning a and b> :~: ) -> Either (<some type-level expression mentioning a and b> :~: ) (a :~: b) Somehow one has to communicate the equation to the compiler that should be proved under the assumption that a is not unifiable with b. Is this clearer? Sorry for the sloppy definition! Cheers, Gabor

...

Richard

Richard Eisenberg

11:39 a.m.

This works for me (with ScopedTypeVariables):

...

gabor :: forall a b lhs rhs. (KnownSymbol a, KnownSymbol b) => Proxy a -> Proxy b -> Proxy (lhs :~: rhs) -> Either (lhs :~: rhs) (a :~: b) gabor a b _ = case sameSymbol a b of Just refl -> Right refl Nothing -> Left (unsafeCoerce Refl)

Does this do what you want? Richard On Jul 27, 2015, at 11:22 AM, Gabor Greif wrote:

...

On 7/27/15, Richard Eisenberg wrote:

...
On Jul 27, 2015, at 10:56 AM, Gabor Greif wrote:

...
...
...
decideRefl :: Proxy (a :: Symbol) -> Proxy b -> Proxy (Equal a b :~: 'False) -> Either (Equal a b :~: 'False) (a :~: b)

What's the point of the third Proxy argument? I don't think it adds anything. Perhaps without that the way forward (albeit still with unsafeCoerce) will become clear.

Proxy (Equal a b :~: 'False) is just the specialised version to the general issue I'd like to crack:

Proxy a -> Proxy b -> Proxy (<some type-level expression mentioning a and b> :~: ) -> Either (<some type-level expression mentioning a and b> :~: ) (a :~: b)

Somehow one has to communicate the equation to the compiler that should be proved under the assumption that a is not unifiable with b.

Is this clearer? Sorry for the sloppy definition!

Cheers,

Gabor

...
Richard

Gabor Greif

12:04 p.m.

On 7/27/15, Richard Eisenberg wrote:

...

This works for me (with ScopedTypeVariables):

...
gabor :: forall a b lhs rhs. (KnownSymbol a, KnownSymbol b) => Proxy a -> Proxy b -> Proxy (lhs :~: rhs) -> Either (lhs :~: rhs) (a :~: b) gabor a b _ = case sameSymbol a b of Just refl -> Right refl Nothing -> Left (unsafeCoerce Refl)

This is basically what I am doing now. Namely using unsafeCoerce. But this is not what I am after. Namely a safe way to exploit negative evidence coming from sameSymbol. I want a (weak form of) decidable type-level equality, where I either get a witness that a and b are equal (just like sameSymbol works now) or alternatively a different witness that a type function evaluates to some type under the assumption that a is not b. This is the interesting part, as the type family could get stuck without this knowledge as my original example illustrates (and also Simon's). The goal is not only to obtain *some* witness, but to never obtain a bad witness this way (i.e. never get something like 'True :~: 'False). Cheers, Gabor

...

Does this do what you want?

Richard

On Jul 27, 2015, at 11:22 AM, Gabor Greif wrote:

...
On 7/27/15, Richard Eisenberg wrote:

...
On Jul 27, 2015, at 10:56 AM, Gabor Greif wrote:

...
...
...
decideRefl :: Proxy (a :: Symbol) -> Proxy b -> Proxy (Equal a b :~: 'False) -> Either (Equal a b :~: 'False) (a :~: b)

What's the point of the third Proxy argument? I don't think it adds anything. Perhaps without that the way forward (albeit still with unsafeCoerce) will become clear.

Proxy (Equal a b :~: 'False) is just the specialised version to the general issue I'd like to crack:

Proxy a -> Proxy b -> Proxy (<some type-level expression mentioning a and b> :~: ) -> Either (<some type-level expression mentioning a and b> :~: ) (a :~: b)

Somehow one has to communicate the equation to the compiler that should be proved under the assumption that a is not unifiable with b.

Is this clearer? Sorry for the sloppy definition!

Cheers,

Gabor

...
Richard

Richard Eisenberg

12:53 p.m.

It sounds like you want this, then:

...

gabor :: forall a b. (KnownSymbol a, KnownSymbol b) => Proxy a -> Proxy b -> Either (Equal a b :~: 'False) (a :~: b) gabor a b = case sameSymbol a b of Just refl -> Right refl Nothing -> Left (unsafeCoerce Refl)

It still uses unsafeCoerce, of course. There isn't really any advantage to baking the use of unsafeCoerce into GHC, as the GHC core would still use unsafeCoerce here. So, I think that -- barring the Big Deal of inventing proper inequality witnesses -- you're a little tied to unsafeCoerce. Richard On Jul 27, 2015, at 12:04 PM, Gabor Greif wrote:

...

On 7/27/15, Richard Eisenberg wrote:

...
This works for me (with ScopedTypeVariables):

...
gabor :: forall a b lhs rhs. (KnownSymbol a, KnownSymbol b) => Proxy a -> Proxy b -> Proxy (lhs :~: rhs) -> Either (lhs :~: rhs) (a :~: b) gabor a b _ = case sameSymbol a b of Just refl -> Right refl Nothing -> Left (unsafeCoerce Refl)

This is basically what I am doing now. Namely using unsafeCoerce.

But this is not what I am after. Namely a safe way to exploit negative evidence coming from sameSymbol. I want a (weak form of) decidable type-level equality, where I either get a witness that a and b are equal (just like sameSymbol works now) or alternatively a different witness that a type function evaluates to some type under the assumption that a is not b. This is the interesting part, as the type family could get stuck without this knowledge as my original example illustrates (and also Simon's).

The goal is not only to obtain *some* witness, but to never obtain a bad witness this way (i.e. never get something like 'True :~: 'False).

Cheers,

Gabor

...
Does this do what you want?

Richard

On Jul 27, 2015, at 11:22 AM, Gabor Greif wrote:

...
On 7/27/15, Richard Eisenberg wrote:

...
On Jul 27, 2015, at 10:56 AM, Gabor Greif wrote:

...
...
> > decideRefl :: Proxy (a :: Symbol) -> Proxy b > -> Proxy (Equal a b :~: 'False) > -> Either (Equal a b :~: 'False) (a :~: b)

What's the point of the third Proxy argument? I don't think it adds anything. Perhaps without that the way forward (albeit still with unsafeCoerce) will become clear.

Proxy (Equal a b :~: 'False) is just the specialised version to the general issue I'd like to crack:

Proxy a -> Proxy b -> Proxy (<some type-level expression mentioning a and b> :~: ) -> Either (<some type-level expression mentioning a and b> :~: ) (a :~: b)

Somehow one has to communicate the equation to the compiler that should be proved under the assumption that a is not unifiable with b.

Is this clearer? Sorry for the sloppy definition!

Cheers,

Gabor

...
Richard

Simon Peyton Jones

12:04 p.m.

| When saying "Big Deal" did you mean | - highly desirable and somebody should go for it | - or a terrible amount of work, and who tackles it is probably a | fool on a hubris trip? I meant - a lot of work, including changes to the core System FC language - we lack enough compelling cases to justify that work But it would certainly be interesting. In short, a research exercise, not an engineering one. Simon

Richard Eisenberg

10:38 a.m.

On Jul 27, 2015, at 9:48 AM, Simon Peyton Jones wrote:

...

Making type inference (and system FC) exploit negative info would be a Big Deal, I think.

Yes. Gabor points out a known infelicity with the interaction between closed type families and GADTs. But I agree with Simon that fixing it would indeed be a Big Deal, and not yet worth the very considerable effort required. Richard

3587

Age (days ago)

3590

Last active (days ago)

List overview

Download

13 comments

4 participants

participants (4)

Anthony Cowley
Gabor Greif
Richard Eisenberg
Simon Peyton Jones