[Haskell-cafe] 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 <78emil at 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
>
> 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.
> >
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20161208/c81ef440/attachment.html>