<html><head><meta http-equiv="Content-Type" content="text/html charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;" class="">The david’s approach is ingenious, but a more direct way, is to construct<div class="">the type equality proof yourself.</div><div class=""><br class=""></div><div class="">It’s more like what it would look like in say Agda:</div><div class=""><br class=""></div><div class=""><div class="">{-# LANGUAGE DataKinds #-}</div><div class="">{-# LANGUAGE GADTs #-}</div><div class="">{-# LANGUAGE RankNTypes #-}</div><div class="">{-# LANGUAGE ScopedTypeVariables #-}</div><div class="">{-# LANGUAGE TypeFamilies #-}</div><div class="">{-# LANGUAGE TypeOperators #-}</div><div class="">{-# OPTIONS_GHC -Wall -Wno-redundant-constraints #-}</div><div class="">import Data.Type.Bool</div><div class="">import Data.Type.Equality</div><div class=""><br class=""></div><div class="">-- <a href="http://hackage.haskell.org/package/singleton-bool-0.1.2.0/docs/Data-Singletons-Bool.html" class="">http://hackage.haskell.org/package/singleton-bool-0.1.2.0/docs/Data-Singletons-Bool.html</a></div><div class="">import Data.Singletons.Bool</div><div class=""><br class=""></div><div class="">import Unsafe.Coerce (unsafeCoerce)</div><div class=""><br class=""></div><div class="">-- Safe version</div><div class="">proof</div><div class=""> :: forall a b. (SBoolI a, SBoolI b, (a || b) ~ 'False)</div><div class=""> => (a :~: 'False, b :~: 'False)</div><div class="">proof = case (sbool :: SBool a, sbool :: SBool b) of</div><div class=""> (SFalse, SFalse) -> (Refl, Refl)</div><div class=""><br class=""></div><div class="">-- with unsafeCoerce we don't need the contexts. they can be satisfied for all a, b :: Bool</div><div class="">-- and we don't want runtime SBool dictionaries hanging around (would need to change Expr definition)</div><div class="">proof'</div><div class=""> :: forall a b. ((a || b) ~ 'False)</div><div class=""> => (a :~: 'False, b :~: 'False)</div><div class="">proof' = (unsafeCoerce trivialRefl, unsafeCoerce trivialRefl)</div><div class=""><br class=""></div><div class="">data Expr t where</div><div class=""> Add :: Expr t -> Expr t' -> Expr (t || t')</div><div class=""> Lit :: Int -> Expr 'False</div><div class=""> Var :: Expr 'True</div><div class=""><br class=""></div><div class="">eval' :: Expr 'False -> Int</div><div class="">eval' (Lit i) = i</div><div class="">eval' (Add a b) = add a b</div><div class=""> where</div><div class=""> add :: forall t t'. ((t || t') ~ 'False) => Expr t -> Expr t' -> Int</div><div class=""> add x y = case proof' :: (t :~: 'False, t' :~: 'False) of</div><div class=""> (Refl, Refl) -> eval' x + eval' y</div></div><div class=""><br class=""></div><div class=""><br class=""><div class=""><div><blockquote type="cite" class=""><div class="">On 07 Dec 2016, at 09:43, Guillaume Bouchard <<a href="mailto:guillaum.bouchard+haskell@gmail.com" class="">guillaum.bouchard+haskell@gmail.com</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><div dir="ltr" class="">Hi.<div class=""><br class=""></div><div class="">I have the following GADT :</div><div class=""><br class=""></div><div class="">-----------------------------</div><div class=""><div class="">type family Or a b where</div><div class=""> Or 'False 'False = 'False</div><div class=""> Or _ _ = 'True</div><div class=""><br class=""></div><div class="">data Expr t where</div><div class=""> Add :: Expr t -> Expr t' -> Expr (Or t t')</div><div class=""> Lit :: Int -> Expr 'False</div><div class=""> Var :: Expr 'True</div></div><div class="">----------------------</div><div class=""><br class=""></div><div class="">The idea is that if the `Expr` contains a sub `Var`, its type is `Expr 'True`, else it is `Expr 'False`.</div><div class=""><br class=""></div><div class="">I now want to evaluate my expression, something like that :</div><div class=""><br class=""></div><div class="">--------------</div><div class=""><div class="">eval :: Expr t -> Int</div><div class="">eval (Lit i) = i</div><div class="">eval (Add a b) = eval a + eval b</div><div class="">eval Var = error "Cannot evaluate expression with variable"</div></div><div class="">----------------</div><div class=""><br class=""></div><div class="">Using the GADT I previously defined, I'm tempted to remove the impossible "Var" case with :</div><div class=""><br class=""></div><div class="">---------------</div><div class=""><div class="">eval' :: Expr 'False -> Int</div><div class="">eval' (Lit i) = i</div><div class="">eval' (Add a b) = eval' a + eval' b</div></div><div class="">----------------</div><div class=""><br class=""></div><div class="">However this does not typecheck because GHC cannot deduce that `a` and `b` are `~ Expr 'False`. Because the type family `Or` is not injective.</div><div class=""><br class=""></div><div class="">The wiki <a href="https://ghc.haskell.org/trac/ghc/wiki/InjectiveTypeFamilies" class="">https://ghc.haskell.org/trac/ghc/wiki/InjectiveTypeFamilies</a> classifies injectives types families in three categories, but I don't think my `Or` appears in any of them.</div><div class=""><br class=""></div><div class="">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".</div><div class=""><br class=""></div><div class="">The type checker does not know that, hence my code does not compile.</div><div class=""><br class=""></div><div class="">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:</div><div class=""><br class=""></div><div class="">type family InverseOr a where</div><div class=""> InverseOr 'False = ('False, 'False)</div><div class=""><br class=""></div><div class="">Thank you.</div><div class=""><br class=""></div><div class="">-- </div><div class="">G.</div></div>
_______________________________________________<br class="">Haskell-Cafe mailing list<br class="">To (un)subscribe, modify options or view archives go to:<br class=""><a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" class="">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br class="">Only members subscribed via the mailman list are allowed to post.</div></blockquote></div><br class=""></div></div></body></html>