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

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" 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 -- http://hackage.haskell.org/package/singleton-bool-0.1.2. 0/docs/Data-Singletons-Bool.html 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 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.

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 <78emil@gmail.com> 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

...

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

Den 2016-12-07 kl. 08:43, skrev Guillaume Bouchard: 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.