<div dir="ltr">Thank you,<div><br></div><div>Emil, your solution is really interesting and helped me to understand the trick in the ST monad.</div><div><br></div><div>David, beautiful and generic solution, thank you.</div><div><br></div><div>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:</div><div><br></div><div>- What about the unsafeCoerce, I don't really understand its need</div><div>- 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 ?</div><div><br></div><div>Thank you.</div></div><br><div class="gmail_quote"><div dir="ltr">Le jeu. 8 déc. 2016 à 11:31, Emil Axelsson <<a href="mailto:78emil@gmail.com">78emil@gmail.com</a>> a écrit :<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">A different way to achieve the guarantee you want is to let unification<br class="gmail_msg">
do the "oring" for you:<br class="gmail_msg">
<br class="gmail_msg">
{-# LANGUAGE GADTs #-}<br class="gmail_msg">
{-# LANGUAGE Rank2Types #-}<br class="gmail_msg">
<br class="gmail_msg">
{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}<br class="gmail_msg">
<br class="gmail_msg">
data HasVar<br class="gmail_msg">
<br class="gmail_msg">
data Expr t where<br class="gmail_msg">
Add :: Expr x -> Expr x -> Expr x<br class="gmail_msg">
Lit :: Int -> Expr x<br class="gmail_msg">
Var :: Expr HasVar<br class="gmail_msg">
<br class="gmail_msg">
eval :: (forall x . Expr x) -> Int<br class="gmail_msg">
eval = go<br class="gmail_msg">
where<br class="gmail_msg">
go :: Expr () -> Int<br class="gmail_msg">
go (Add a b) = go a + go b<br class="gmail_msg">
go (Lit a) = a<br class="gmail_msg">
<br class="gmail_msg">
/ Emil<br class="gmail_msg">
<br class="gmail_msg">
Den 2016-12-07 kl. 08:43, skrev Guillaume Bouchard:<br class="gmail_msg">
> Hi.<br class="gmail_msg">
><br class="gmail_msg">
> I have the following GADT :<br class="gmail_msg">
><br class="gmail_msg">
> -----------------------------<br class="gmail_msg">
> type family Or a b where<br class="gmail_msg">
> Or 'False 'False = 'False<br class="gmail_msg">
> Or _ _ = 'True<br class="gmail_msg">
><br class="gmail_msg">
> data Expr t where<br class="gmail_msg">
> Add :: Expr t -> Expr t' -> Expr (Or t t')<br class="gmail_msg">
> Lit :: Int -> Expr 'False<br class="gmail_msg">
> Var :: Expr 'True<br class="gmail_msg">
> ----------------------<br class="gmail_msg">
><br class="gmail_msg">
> The idea is that if the `Expr` contains a sub `Var`, its type is `Expr 'True`,<br class="gmail_msg">
> else it is `Expr 'False`.<br class="gmail_msg">
><br class="gmail_msg">
> I now want to evaluate my expression, something like that :<br class="gmail_msg">
><br class="gmail_msg">
> --------------<br class="gmail_msg">
> eval :: Expr t -> Int<br class="gmail_msg">
> eval (Lit i) = i<br class="gmail_msg">
> eval (Add a b) = eval a + eval b<br class="gmail_msg">
> eval Var = error "Cannot evaluate expression with variable"<br class="gmail_msg">
> ----------------<br class="gmail_msg">
><br class="gmail_msg">
> Using the GADT I previously defined, I'm tempted to remove the impossible "Var"<br class="gmail_msg">
> case with :<br class="gmail_msg">
><br class="gmail_msg">
> ---------------<br class="gmail_msg">
> eval' :: Expr 'False -> Int<br class="gmail_msg">
> eval' (Lit i) = i<br class="gmail_msg">
> eval' (Add a b) = eval' a + eval' b<br class="gmail_msg">
> ----------------<br class="gmail_msg">
><br class="gmail_msg">
> However this does not typecheck because GHC cannot deduce that `a` and `b` are<br class="gmail_msg">
> `~ Expr 'False`. Because the type family `Or` is not injective.<br class="gmail_msg">
><br class="gmail_msg">
> The wiki <a href="https://ghc.haskell.org/trac/ghc/wiki/InjectiveTypeFamilies" rel="noreferrer" class="gmail_msg" target="_blank">https://ghc.haskell.org/trac/ghc/wiki/InjectiveTypeFamilies</a> classifies<br class="gmail_msg">
> injectives types families in three categories, but I don't think my `Or` appears<br class="gmail_msg">
> in any of them.<br class="gmail_msg">
><br class="gmail_msg">
> Actually `Or` is injective only if `Or t t' ~ 'False` and in this case, we can<br class="gmail_msg">
> deduce that `t ~ 'False` and `t' ~ 'False`. I qualify it as a "partialy<br class="gmail_msg">
> injective type family".<br class="gmail_msg">
><br class="gmail_msg">
> The type checker does not know that, hence my code does not compile.<br class="gmail_msg">
><br class="gmail_msg">
> Is there a solution, other than writing a custom type checker plugin? Is there a<br class="gmail_msg">
> way to provide the inverse type family function, something such as:<br class="gmail_msg">
><br class="gmail_msg">
> type family InverseOr a where<br class="gmail_msg">
> InverseOr 'False = ('False, 'False)<br class="gmail_msg">
><br class="gmail_msg">
> Thank you.<br class="gmail_msg">
><br class="gmail_msg">
> --<br class="gmail_msg">
> G.<br class="gmail_msg">
><br class="gmail_msg">
><br class="gmail_msg">
><br class="gmail_msg">
> _______________________________________________<br class="gmail_msg">
> Haskell-Cafe mailing list<br class="gmail_msg">
> To (un)subscribe, modify options or view archives go to:<br class="gmail_msg">
> <a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" rel="noreferrer" class="gmail_msg" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br class="gmail_msg">
> Only members subscribed via the mailman list are allowed to post.<br class="gmail_msg">
><br class="gmail_msg">
</blockquote></div>