Re: [Haskell-cafe] Injective type family on a sub domain

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 -- http://hackage.haskell.org/package/singleton-bool-0.1.2.0/docs/Data-Singleto... 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 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 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.