[Haskell-cafe] Injective type family on a sub domain
David Feuer
david.feuer at gmail.com
Thu Dec 8 02:51:21 UTC 2016
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" <david.feuer at gmail.com> wrote:
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" <david.feuer at gmail.com> wrote:
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" <guillaum.bouchard+haskell at gma
il.com> wrote:
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/20161207/4d0b902b/attachment.html>
More information about the Haskell-Cafe
mailing list