Injective type family on a sub domain

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
8 messages Options
Reply | Threaded
Open this post in threaded view
|

Injective type family on a sub domain

Guillaume Bouchard
Hi.

I have the following GADT :

-----------------------------
type family Or a b where
  Or 'False 'False = 'False
  Or _ _ = 'True

data Expr t where
  Add :: Expr t -> Expr t' -> Expr (Or t t')
  Lit :: Int -> Expr 'False
  Var :: Expr 'True
----------------------

The idea is that if the `Expr` contains a sub `Var`, its type is `Expr 'True`, else it is `Expr 'False`.

I now want to evaluate my expression, something like that :

--------------
eval :: Expr t -> Int
eval (Lit i) = i
eval (Add a b) = eval a + eval b
eval Var = error "Cannot evaluate expression with variable"
----------------

Using the GADT I previously defined, I'm tempted to remove the impossible "Var" case with :

---------------
eval' :: Expr 'False -> Int
eval' (Lit i) = i
eval' (Add a b) = eval' a + eval' b
----------------

However this does not typecheck because GHC cannot deduce that `a` and `b` are `~ Expr 'False`. Because the type family `Or` is not injective.

The wiki https://ghc.haskell.org/trac/ghc/wiki/InjectiveTypeFamilies classifies injectives types families in three categories, but I don't think my `Or` appears in any of them.

Actually `Or` is injective only if `Or t t' ~ 'False` and in this case, we can deduce that `t ~ 'False` and `t' ~ 'False`. I qualify it as a "partialy injective type family".

The type checker does not know that, hence my code does not compile.

Is there a solution, other than writing a custom type checker plugin? Is there a way to provide the inverse type family function, something such as:

type family InverseOr a where
     InverseOr 'False = ('False, 'False)

Thank you.

-- 
G.

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Injective type family on a sub domain

David Feuer
Yes, you can do this. Enable ConstraintKinds, import Data.Type.Bool and something exporting Constraint, and change your Add constructor to

Add :: (r ~ Or t t', If (Not r) (t ~ 'False, t' ~ 'False) (() :: Constraint) => Expr t -> Expr t' -> Expr r

Then both eval and eval' are accepted. There may be some cleaner way; I'm no expert.


On Dec 7, 2016 2:43 AM, "Guillaume Bouchard" <[hidden email]> wrote:
Hi.

I have the following GADT :

-----------------------------
type family Or a b where
  Or 'False 'False = 'False
  Or _ _ = 'True

data Expr t where
  Add :: Expr t -> Expr t' -> Expr (Or t t')
  Lit :: Int -> Expr 'False
  Var :: Expr 'True
----------------------

The idea is that if the `Expr` contains a sub `Var`, its type is `Expr 'True`, else it is `Expr 'False`.

I now want to evaluate my expression, something like that :

--------------
eval :: Expr t -> Int
eval (Lit i) = i
eval (Add a b) = eval a + eval b
eval Var = error "Cannot evaluate expression with variable"
----------------

Using the GADT I previously defined, I'm tempted to remove the impossible "Var" case with :

---------------
eval' :: Expr 'False -> Int
eval' (Lit i) = i
eval' (Add a b) = eval' a + eval' b
----------------

However this does not typecheck because GHC cannot deduce that `a` and `b` are `~ Expr 'False`. Because the type family `Or` is not injective.

The wiki https://ghc.haskell.org/trac/ghc/wiki/InjectiveTypeFamilies classifies injectives types families in three categories, but I don't think my `Or` appears in any of them.

Actually `Or` is injective only if `Or t t' ~ 'False` and in this case, we can deduce that `t ~ 'False` and `t' ~ 'False`. I qualify it as a "partialy injective type family".

The type checker does not know that, hence my code does not compile.

Is there a solution, other than writing a custom type checker plugin? Is there a way to provide the inverse type family function, something such as:

type family InverseOr a where
     InverseOr 'False = ('False, 'False)

Thank you.

-- 
G.

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.


_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Injective type family on a sub domain

David Feuer
Er... There's a missing close paren at the end of the context; sorry. That should be

Add :: (r ~ Or t t', If (Not r) (t ~ 'False, t' ~ 'False) (() :: Constraint)) => Expr t -> Expr t' -> Expr r

On Dec 7, 2016 9:16 PM, "David Feuer" <[hidden email]> wrote:
Yes, you can do this. Enable ConstraintKinds, import Data.Type.Bool and something exporting Constraint, and change your Add constructor to

Add :: (r ~ Or t t', If (Not r) (t ~ 'False, t' ~ 'False) (() :: Constraint) => Expr t -> Expr t' -> Expr r

Then both eval and eval' are accepted. There may be some cleaner way; I'm no expert.


On Dec 7, 2016 2:43 AM, "Guillaume Bouchard" <[hidden email]> wrote:
Hi.

I have the following GADT :

-----------------------------
type family Or a b where
  Or 'False 'False = 'False
  Or _ _ = 'True

data Expr t where
  Add :: Expr t -> Expr t' -> Expr (Or t t')
  Lit :: Int -> Expr 'False
  Var :: Expr 'True
----------------------

The idea is that if the `Expr` contains a sub `Var`, its type is `Expr 'True`, else it is `Expr 'False`.

I now want to evaluate my expression, something like that :

--------------
eval :: Expr t -> Int
eval (Lit i) = i
eval (Add a b) = eval a + eval b
eval Var = error "Cannot evaluate expression with variable"
----------------

Using the GADT I previously defined, I'm tempted to remove the impossible "Var" case with :

---------------
eval' :: Expr 'False -> Int
eval' (Lit i) = i
eval' (Add a b) = eval' a + eval' b
----------------

However this does not typecheck because GHC cannot deduce that `a` and `b` are `~ Expr 'False`. Because the type family `Or` is not injective.

The wiki https://ghc.haskell.org/trac/ghc/wiki/InjectiveTypeFamilies classifies injectives types families in three categories, but I don't think my `Or` appears in any of them.

Actually `Or` is injective only if `Or t t' ~ 'False` and in this case, we can deduce that `t ~ 'False` and `t' ~ 'False`. I qualify it as a "partialy injective type family".

The type checker does not know that, hence my code does not compile.

Is there a solution, other than writing a custom type checker plugin? Is there a way to provide the inverse type family function, something such as:

type family InverseOr a where
     InverseOr 'False = ('False, 'False)

Thank you.

-- 
G.

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.



_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Injective type family on a sub domain

David Feuer
While you're at it, you should probably add the rest of the implications:

If (r && Not t) (t' ~ 'True) (() :: Constraint),
If (r && Not t') (t ~ 'True) (() :: Constraint)

On Dec 7, 2016 9:18 PM, "David Feuer" <[hidden email]> wrote:
Er... There's a missing close paren at the end of the context; sorry. That should be

Add :: (r ~ Or t t', If (Not r) (t ~ 'False, t' ~ 'False) (() :: Constraint)) => Expr t -> Expr t' -> Expr r


On Dec 7, 2016 9:16 PM, "David Feuer" <[hidden email]> wrote:
Yes, you can do this. Enable ConstraintKinds, import Data.Type.Bool and something exporting Constraint, and change your Add constructor to

Add :: (r ~ Or t t', If (Not r) (t ~ 'False, t' ~ 'False) (() :: Constraint) => Expr t -> Expr t' -> Expr r

Then both eval and eval' are accepted. There may be some cleaner way; I'm no expert.


On Dec 7, 2016 2:43 AM, "Guillaume Bouchard" <[hidden email]> wrote:
Hi.

I have the following GADT :

-----------------------------
type family Or a b where
  Or 'False 'False = 'False
  Or _ _ = 'True

data Expr t where
  Add :: Expr t -> Expr t' -> Expr (Or t t')
  Lit :: Int -> Expr 'False
  Var :: Expr 'True
----------------------

The idea is that if the `Expr` contains a sub `Var`, its type is `Expr 'True`, else it is `Expr 'False`.

I now want to evaluate my expression, something like that :

--------------
eval :: Expr t -> Int
eval (Lit i) = i
eval (Add a b) = eval a + eval b
eval Var = error "Cannot evaluate expression with variable"
----------------

Using the GADT I previously defined, I'm tempted to remove the impossible "Var" case with :

---------------
eval' :: Expr 'False -> Int
eval' (Lit i) = i
eval' (Add a b) = eval' a + eval' b
----------------

However this does not typecheck because GHC cannot deduce that `a` and `b` are `~ Expr 'False`. Because the type family `Or` is not injective.

The wiki https://ghc.haskell.org/trac/ghc/wiki/InjectiveTypeFamilies classifies injectives types families in three categories, but I don't think my `Or` appears in any of them.

Actually `Or` is injective only if `Or t t' ~ 'False` and in this case, we can deduce that `t ~ 'False` and `t' ~ 'False`. I qualify it as a "partialy injective type family".

The type checker does not know that, hence my code does not compile.

Is there a solution, other than writing a custom type checker plugin? Is there a way to provide the inverse type family function, something such as:

type family InverseOr a where
     InverseOr 'False = ('False, 'False)

Thank you.

-- 
G.

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.




_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Injective type family on a sub domain

Oleg Grenrus
In reply to this post by Guillaume Bouchard
The david’s approach is ingenious, but a more direct way, is to construct
the type equality proof yourself.

It’s more like what it would look like in say Agda:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -Wall -Wno-redundant-constraints #-}
import Data.Type.Bool
import Data.Type.Equality

import Data.Singletons.Bool

import Unsafe.Coerce (unsafeCoerce)

-- Safe version
proof
    :: forall a b. (SBoolI a, SBoolI b, (a || b) ~ 'False)
    => (a :~: 'False, b :~: 'False)
proof = case (sbool :: SBool a, sbool :: SBool b) of
    (SFalse, SFalse) -> (Refl, Refl)

-- with unsafeCoerce we don't need the contexts. they can be satisfied for all a, b :: Bool
-- and we don't want runtime SBool dictionaries hanging around (would need to change Expr definition)
proof'
    :: forall a b. ((a || b) ~ 'False)
    => (a :~: 'False, b :~: 'False)
proof' = (unsafeCoerce trivialRefl, unsafeCoerce trivialRefl)

data Expr t where
    Add :: Expr t -> Expr t' -> Expr (t || t')
    Lit :: Int -> Expr 'False
    Var :: Expr 'True

eval' :: Expr 'False -> Int
eval' (Lit i) = i
eval' (Add a b) = add a b
  where
    add :: forall t t'. ((t || t') ~ 'False) => Expr t -> Expr t' ->  Int
    add x y = case proof' :: (t :~: 'False, t' :~: 'False) of
        (Refl, Refl) -> eval' x + eval' y


On 07 Dec 2016, at 09:43, Guillaume Bouchard <[hidden email]> wrote:

Hi.

I have the following GADT :

-----------------------------
type family Or a b where
  Or 'False 'False = 'False
  Or _ _ = 'True

data Expr t where
  Add :: Expr t -> Expr t' -> Expr (Or t t')
  Lit :: Int -> Expr 'False
  Var :: Expr 'True
----------------------

The idea is that if the `Expr` contains a sub `Var`, its type is `Expr 'True`, else it is `Expr 'False`.

I now want to evaluate my expression, something like that :

--------------
eval :: Expr t -> Int
eval (Lit i) = i
eval (Add a b) = eval a + eval b
eval Var = error "Cannot evaluate expression with variable"
----------------

Using the GADT I previously defined, I'm tempted to remove the impossible "Var" case with :

---------------
eval' :: Expr 'False -> Int
eval' (Lit i) = i
eval' (Add a b) = eval' a + eval' b
----------------

However this does not typecheck because GHC cannot deduce that `a` and `b` are `~ Expr 'False`. Because the type family `Or` is not injective.

The wiki https://ghc.haskell.org/trac/ghc/wiki/InjectiveTypeFamilies classifies injectives types families in three categories, but I don't think my `Or` appears in any of them.

Actually `Or` is injective only if `Or t t' ~ 'False` and in this case, we can deduce that `t ~ 'False` and `t' ~ 'False`. I qualify it as a "partialy injective type family".

The type checker does not know that, hence my code does not compile.

Is there a solution, other than writing a custom type checker plugin? Is there a way to provide the inverse type family function, something such as:

type family InverseOr a where
     InverseOr 'False = ('False, 'False)

Thank you.

-- 
G.
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.


_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.

signature.asc (859 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|

Re: Injective type family on a sub domain

David Feuer
Another option, I believe, would be to include singletons (or constraints providing them) to the Add constructor.

On Dec 8, 2016 3:13 AM, "Oleg Grenrus" <[hidden email]> wrote:
The david’s approach is ingenious, but a more direct way, is to construct
the type equality proof yourself.

It’s more like what it would look like in say Agda:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -Wall -Wno-redundant-constraints #-}
import Data.Type.Bool
import Data.Type.Equality

import Data.Singletons.Bool

import Unsafe.Coerce (unsafeCoerce)

-- Safe version
proof
    :: forall a b. (SBoolI a, SBoolI b, (a || b) ~ 'False)
    => (a :~: 'False, b :~: 'False)
proof = case (sbool :: SBool a, sbool :: SBool b) of
    (SFalse, SFalse) -> (Refl, Refl)

-- with unsafeCoerce we don't need the contexts. they can be satisfied for all a, b :: Bool
-- and we don't want runtime SBool dictionaries hanging around (would need to change Expr definition)
proof'
    :: forall a b. ((a || b) ~ 'False)
    => (a :~: 'False, b :~: 'False)
proof' = (unsafeCoerce trivialRefl, unsafeCoerce trivialRefl)

data Expr t where
    Add :: Expr t -> Expr t' -> Expr (t || t')
    Lit :: Int -> Expr 'False
    Var :: Expr 'True

eval' :: Expr 'False -> Int
eval' (Lit i) = i
eval' (Add a b) = add a b
  where
    add :: forall t t'. ((t || t') ~ 'False) => Expr t -> Expr t' ->  Int
    add x y = case proof' :: (t :~: 'False, t' :~: 'False) of
        (Refl, Refl) -> eval' x + eval' y


On 07 Dec 2016, at 09:43, Guillaume Bouchard <[hidden email]> wrote:

Hi.

I have the following GADT :

-----------------------------
type family Or a b where
  Or 'False 'False = 'False
  Or _ _ = 'True

data Expr t where
  Add :: Expr t -> Expr t' -> Expr (Or t t')
  Lit :: Int -> Expr 'False
  Var :: Expr 'True
----------------------

The idea is that if the `Expr` contains a sub `Var`, its type is `Expr 'True`, else it is `Expr 'False`.

I now want to evaluate my expression, something like that :

--------------
eval :: Expr t -> Int
eval (Lit i) = i
eval (Add a b) = eval a + eval b
eval Var = error "Cannot evaluate expression with variable"
----------------

Using the GADT I previously defined, I'm tempted to remove the impossible "Var" case with :

---------------
eval' :: Expr 'False -> Int
eval' (Lit i) = i
eval' (Add a b) = eval' a + eval' b
----------------

However this does not typecheck because GHC cannot deduce that `a` and `b` are `~ Expr 'False`. Because the type family `Or` is not injective.

The wiki https://ghc.haskell.org/trac/ghc/wiki/InjectiveTypeFamilies classifies injectives types families in three categories, but I don't think my `Or` appears in any of them.

Actually `Or` is injective only if `Or t t' ~ 'False` and in this case, we can deduce that `t ~ 'False` and `t' ~ 'False`. I qualify it as a "partialy injective type family".

The type checker does not know that, hence my code does not compile.

Is there a solution, other than writing a custom type checker plugin? Is there a way to provide the inverse type family function, something such as:

type family InverseOr a where
     InverseOr 'False = ('False, 'False)

Thank you.

-- 
G.
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.


_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.


_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Injective type family on a sub domain

Emil Axelsson-3
In reply to this post by Guillaume Bouchard
A different way to achieve the guarantee you want is to let unification
do the "oring" for you:

   {-# LANGUAGE GADTs #-}
   {-# LANGUAGE Rank2Types #-}

   {-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

   data HasVar

   data Expr t where
      Add :: Expr x -> Expr x -> Expr x
      Lit :: Int -> Expr x
      Var :: Expr HasVar

   eval :: (forall x . Expr x) -> Int
   eval = go
     where
       go :: Expr () -> Int
       go (Add a b) = go a + go b
       go (Lit a)   = a

/ Emil

Den 2016-12-07 kl. 08:43, skrev Guillaume Bouchard:

> Hi.
>
> I have the following GADT :
>
> -----------------------------
> type family Or a b where
>    Or 'False 'False = 'False
>    Or _ _ = 'True
>
> data Expr t where
>    Add :: Expr t -> Expr t' -> Expr (Or t t')
>    Lit :: Int -> Expr 'False
>    Var :: Expr 'True
> ----------------------
>
> The idea is that if the `Expr` contains a sub `Var`, its type is `Expr 'True`,
> else it is `Expr 'False`.
>
> I now want to evaluate my expression, something like that :
>
> --------------
> eval :: Expr t -> Int
> eval (Lit i) = i
> eval (Add a b) = eval a + eval b
> eval Var = error "Cannot evaluate expression with variable"
> ----------------
>
> Using the GADT I previously defined, I'm tempted to remove the impossible "Var"
> case with :
>
> ---------------
> eval' :: Expr 'False -> Int
> eval' (Lit i) = i
> eval' (Add a b) = eval' a + eval' b
> ----------------
>
> However this does not typecheck because GHC cannot deduce that `a` and `b` are
> `~ Expr 'False`. Because the type family `Or` is not injective.
>
> The wiki https://ghc.haskell.org/trac/ghc/wiki/InjectiveTypeFamilies classifies
> injectives types families in three categories, but I don't think my `Or` appears
> in any of them.
>
> Actually `Or` is injective only if `Or t t' ~ 'False` and in this case, we can
> deduce that `t ~ 'False` and `t' ~ 'False`. I qualify it as a "partialy
> injective type family".
>
> The type checker does not know that, hence my code does not compile.
>
> Is there a solution, other than writing a custom type checker plugin? Is there a
> way to provide the inverse type family function, something such as:
>
> type family InverseOr a where
>       InverseOr 'False = ('False, 'False)
>
> Thank you.
>
> --
> G.
>
>
>
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.
>
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Injective type family on a sub domain

Guillaume Bouchard
Thank you,

Emil, your solution is really interesting and helped me to understand the trick in the ST monad.

David, beautiful and generic solution, thank you.

Oleg, I live your solution because it does not leak the implementation details of the eval function in the type. However this solution melted my brain and I now have more question than I previously had. The most important ones are:

- What about the unsafeCoerce, I don't really understand its need
- The case statement (in proof and add) let me think that the process is done at runtime. However it is clear that it is a compile time process and that the case always succeed. So I'm lost. Could you elaborate a bit on this ?

Thank you.

Le jeu. 8 déc. 2016 à 11:31, Emil Axelsson <[hidden email]> a écrit :
A different way to achieve the guarantee you want is to let unification
do the "oring" for you:

   {-# LANGUAGE GADTs #-}
   {-# LANGUAGE Rank2Types #-}

   {-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

   data HasVar

   data Expr t where
      Add :: Expr x -> Expr x -> Expr x
      Lit :: Int -> Expr x
      Var :: Expr HasVar

   eval :: (forall x . Expr x) -> Int
   eval = go
     where
       go :: Expr () -> Int
       go (Add a b) = go a + go b
       go (Lit a)   = a

/ Emil

Den 2016-12-07 kl. 08:43, skrev Guillaume Bouchard:
> Hi.
>
> I have the following GADT :
>
> -----------------------------
> type family Or a b where
>    Or 'False 'False = 'False
>    Or _ _ = 'True
>
> data Expr t where
>    Add :: Expr t -> Expr t' -> Expr (Or t t')
>    Lit :: Int -> Expr 'False
>    Var :: Expr 'True
> ----------------------
>
> The idea is that if the `Expr` contains a sub `Var`, its type is `Expr 'True`,
> else it is `Expr 'False`.
>
> I now want to evaluate my expression, something like that :
>
> --------------
> eval :: Expr t -> Int
> eval (Lit i) = i
> eval (Add a b) = eval a + eval b
> eval Var = error "Cannot evaluate expression with variable"
> ----------------
>
> Using the GADT I previously defined, I'm tempted to remove the impossible "Var"
> case with :
>
> ---------------
> eval' :: Expr 'False -> Int
> eval' (Lit i) = i
> eval' (Add a b) = eval' a + eval' b
> ----------------
>
> However this does not typecheck because GHC cannot deduce that `a` and `b` are
> `~ Expr 'False`. Because the type family `Or` is not injective.
>
> The wiki https://ghc.haskell.org/trac/ghc/wiki/InjectiveTypeFamilies classifies
> injectives types families in three categories, but I don't think my `Or` appears
> in any of them.
>
> Actually `Or` is injective only if `Or t t' ~ 'False` and in this case, we can
> deduce that `t ~ 'False` and `t' ~ 'False`. I qualify it as a "partialy
> injective type family".
>
> The type checker does not know that, hence my code does not compile.
>
> Is there a solution, other than writing a custom type checker plugin? Is there a
> way to provide the inverse type family function, something such as:
>
> type family InverseOr a where
>       InverseOr 'False = ('False, 'False)
>
> Thank you.
>
> --
> G.
>
>
>
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.
>

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.