module SubHask.SubType
( (<:) (..)
, Sup
, Embed (..)
, embedType
, embedType1
, embedType2
, mkSubtype
, mkSubtypeInstance
)
where
import Control.Monad
import Language.Haskell.TH
import Language.Haskell.TH.Quote
import SubHask.Internal.Prelude
import Prelude
toRational :: (a <: Rational) => a -> Rational
toRational = embedType
class Sup (s::k) (t::k) (u::k) | s t -> u
instance Sup s s s
class (s :: k) <: (t :: k) where
embedType_ :: Embed s t
data family Embed (s::k) (t::k)
newtype instance Embed (s :: *) (t :: *)
= Embed0 { unEmbed0 :: s -> t }
embedType :: (s <: t) => s -> t
embedType = unEmbed0 embedType_
instance (a :: *) <: (a :: *) where
embedType_ = Embed0 $ id
newtype instance Embed (s :: ka -> *) (t :: ka -> *)
= Embed1 { unEmbed1 :: forall a. s a -> t a }
embedType1 :: (s <: t) => s a -> t a
embedType1 = unEmbed1 embedType_
instance (a :: k1 -> *) <: (a :: k1 -> *) where
embedType_ = Embed1 $ id
newtype instance Embed (s :: ka -> kb -> *) (t :: ka -> kb -> *)
= Embed2 { unEmbed2 :: forall a b. s a b -> t a b}
embedType2 :: (s <: t) => s a b -> t a b
embedType2 = unEmbed2 embedType_
instance (a :: k1 -> k2 -> *) <: (a :: k1 -> k2 -> *) where
embedType_ = Embed2 $ id
law_Subtype_f1 ::
( a <: b
, Eq b
, ctx a
, ctx b
) => proxy ctx
-> b
-> (forall c. ctx c => c -> c)
-> a
-> Bool
law_Subtype_f1 _ b f a = embedType (f a) == f (embedType a) `asTypeOf` b
law_Subtype_f2 ::
( a <: b
, Eq b
, ctx a
, ctx b
) => proxy ctx
-> b
-> (forall c. ctx c => c -> c -> c)
-> a
-> a
-> Bool
law_Subtype_f2 _ b f a1 a2 = embedType (f a1 a2) == f (embedType a1) (embedType a2) `asTypeOf` b
type family a == b :: Bool where
a == a = True
a == b = False
type family If (a::Bool) (b::k) (c::k) :: k where
If True b c = b
If False b c = c
type family When (a::Bool) (b::Constraint) :: Constraint where
When True b = b
When False b = ()
apEmbedType1 ::
( a1 <: b1
) => (b1 -> c) -> a1 -> c
apEmbedType1 f a = f (embedType a)
apEmbedType2 ::
( a1 <: b1
, a2 <: b2
, When (b1==b2) (Sup a1 a2 b1)
) => (b1 -> b2 -> c)
-> (a1 -> a2 -> c)
apEmbedType2 f a b = f (embedType a) (embedType b)
mkSubtype :: Q Type -> Q Type -> Name -> Q [Dec]
mkSubtype qt1 qt2 f = do
t1 <- liftM stripForall qt1
t2 <- liftM stripForall qt2
return $ mkSubtypeInstance t1 t2 f:mkSup t1 t2 t2
stripForall :: Type -> Type
stripForall (ForallT _ _ t) = stripForall t
stripForall (VarT t) = VarT $ mkName $ nameBase t
stripForall (ConT t) = ConT t
stripForall (AppT t1 t2) = AppT (stripForall t1) (stripForall t2)
mkSubtypeInstance :: Type -> Type -> Name -> Dec
mkSubtypeInstance t1 t2 f = InstanceD
[]
( AppT
( AppT
( ConT $ mkName "<:" )
t1
)
t2
)
[ FunD
( mkName "embedType_" )
[ Clause
[]
( NormalB $ AppE
( ConE $ mkName "Embed0" )
( VarE f )
)
[]
]
]
mkSup :: Type -> Type -> Type -> [Dec]
mkSup t1 t2 t3 =
[ InstanceD [] (AppT (AppT (AppT (ConT $ mkName "Sup") t1) t2) t3) []
, InstanceD [] (AppT (AppT (AppT (ConT $ mkName "Sup") t2) t1) t3) []
]