[Haskell-cafe] Injective type family on a sub domain
Oleg Grenrus
oleg.grenrus at iki.fi
Thu Dec 8 08:13:06 UTC 2016
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
-- http://hackage.haskell.org/package/singleton-bool-0.1.2.0/docs/Data-Singletons-Bool.html
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
> On 07 Dec 2016, at 09:43, Guillaume Bouchard <guillaum.bouchard+haskell at gmail.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 <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/26f9fa78/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 842 bytes
Desc: Message signed with OpenPGP using GPGMail
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20161208/26f9fa78/attachment.sig>
More information about the Haskell-Cafe
mailing list