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. |
Yes, you can do this. Enable ConstraintKinds, import Data.Type.Bool and something exporting Constraint, and change your Add constructor to
Add :: (r ~ Or t t', If (Not r) (t ~ 'False, t' ~ 'False) (() :: Constraint) => Expr t -> Expr t' -> Expr r Then both eval and eval' are accepted. There may be some cleaner way; I'm no expert. On Dec 7, 2016 2:43 AM, "Guillaume Bouchard" <[hidden email]> wrote:
_______________________________________________ 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. |
Er... There's a missing close paren at the end of the context; sorry. That should be Add :: (r ~ Or t t', If (Not r) (t ~ 'False, t' ~ 'False) (() :: Constraint)) => Expr t -> Expr t' -> Expr r On Dec 7, 2016 9:16 PM, "David Feuer" <[hidden email]> wrote:
_______________________________________________ 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. |
While you're at it, you should probably add the rest of the implications:
If (r && Not t) (t' ~ 'True) (() :: Constraint), If (r && Not t') (t ~ 'True) (() :: Constraint) On Dec 7, 2016 9:18 PM, "David Feuer" <[hidden email]> wrote:
_______________________________________________ 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. |
In reply to this post by Guillaume Bouchard
The david’s approach is ingenious, but a more direct way, is to construct
the type equality proof yourself. It’s more like what it would look like in say Agda: {-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# OPTIONS_GHC -Wall -Wno-redundant-constraints #-} import Data.Type.Bool import Data.Type.Equality import Data.Singletons.Bool import Unsafe.Coerce (unsafeCoerce) -- Safe version proof :: forall a b. (SBoolI a, SBoolI b, (a || b) ~ 'False) => (a :~: 'False, b :~: 'False) proof = case (sbool :: SBool a, sbool :: SBool b) of (SFalse, SFalse) -> (Refl, Refl) -- with unsafeCoerce we don't need the contexts. they can be satisfied for all a, b :: Bool -- and we don't want runtime SBool dictionaries hanging around (would need to change Expr definition) proof' :: forall a b. ((a || b) ~ 'False) => (a :~: 'False, b :~: 'False) proof' = (unsafeCoerce trivialRefl, unsafeCoerce trivialRefl) data Expr t where Add :: Expr t -> Expr t' -> Expr (t || t') Lit :: Int -> Expr 'False Var :: Expr 'True eval' :: Expr 'False -> Int eval' (Lit i) = i eval' (Add a b) = add a b where add :: forall t t'. ((t || t') ~ 'False) => Expr t -> Expr t' -> Int add x y = case proof' :: (t :~: 'False, t' :~: 'False) of (Refl, Refl) -> eval' x + eval' y
_______________________________________________ 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. signature.asc (859 bytes) Download Attachment |
Another option, I believe, would be to include singletons (or constraints providing them) to the Add constructor. On Dec 8, 2016 3:13 AM, "Oleg Grenrus" <[hidden email]> wrote:
_______________________________________________ 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. |
In reply to this post by Guillaume Bouchard
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. > 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. |
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 <[hidden email]> a écrit : A different way to achieve the guarantee you want is to let unification _______________________________________________ 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. |
Free forum by Nabble | Edit this page |