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.