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

[Emil Axelsson]

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