Last active
May 21, 2018 12:55
-
-
Save RyanGlScott/a1abb0496579e07dcd51e358a94c0219 to your computer and use it in GitHub Desktop.
Dependent composition?
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# LANGUAGE AllowAmbiguousTypes #-} | |
{-# LANGUAGE CPP #-} | |
{-# LANGUAGE FlexibleContexts #-} | |
{-# LANGUAGE FlexibleInstances #-} | |
{-# LANGUAGE GADTs #-} | |
{-# LANGUAGE RankNTypes #-} | |
{-# LANGUAGE ScopedTypeVariables #-} | |
{-# LANGUAGE TypeApplications #-} | |
{-# LANGUAGE TypeFamilyDependencies #-} | |
{-# LANGUAGE TypeInType #-} | |
{-# LANGUAGE TypeOperators #-} | |
module DependentComposition where | |
import Data.Kind | |
import Data.Proxy | |
data family Sing (a :: k) | |
data SomeSing :: Type -> Type where | |
SomeSing :: Sing (a :: k) -> SomeSing k | |
class SingKind k where | |
type Demote k = (r :: Type) | r -> k | |
fromSing :: Sing (a :: k) -> Demote k | |
toSing :: Demote k -> SomeSing k | |
withSomeSing :: forall k r | |
. SingKind k | |
=> Demote k | |
-> (forall (a :: k). Sing a -> r) | |
-> r | |
withSomeSing x f = | |
case toSing x of | |
SomeSing x' -> f x' | |
newtype instance Sing (f :: k1 ~> k2) = | |
SLambda { applySing :: forall t. Sing t -> Sing (f @@ t) } | |
instance (SingKind k1, SingKind k2) => SingKind (k1 ~> k2) where | |
type Demote (k1 ~> k2) = Demote k1 -> Demote k2 | |
fromSing sFun x = withSomeSing x (fromSing . applySing sFun) | |
toSing = undefined | |
data TyFun :: Type -> Type -> Type | |
type a ~> b = TyFun a b -> Type | |
infixr 0 ~> | |
type family Apply (f :: k1 ~> k2) (x :: k1) :: k2 | |
type f @@ x = Apply f x | |
infixl 9 @@ | |
dapply1 :: forall (a :: Type) | |
(b :: a ~> Type) | |
(x :: a). | |
(forall (x :: a). b @@ x) | |
-> Sing x | |
-> b @@ x | |
dapply1 f _ = f @x | |
dapply2 :: forall (a :: Type) | |
(b :: a ~> Type) | |
(f :: forall (x :: a). Proxy x ~> b @@ x) | |
(x :: a). | |
SingKind (b @@ x) | |
=> (forall (xx :: a). Sing (f @@ ('Proxy :: Proxy xx))) | |
-> Sing x | |
-> Demote (b @@ x) | |
dapply2 sf _ = fromSing $ sf @x | |
dcomp1 :: forall (a :: Type) | |
(b :: a ~> Type) | |
(c :: forall (x :: a). Proxy x ~> b @@ x ~> Type) | |
(g :: forall (x :: a). Proxy x ~> b @@ x) | |
(x :: a). | |
(forall (xx :: a) (yy :: b @@ xx). c @@ ('Proxy :: Proxy xx) @@ yy) | |
-> (forall (xx :: a). Sing (g @@ ('Proxy :: Proxy xx))) | |
-> Sing x | |
-> c @@ ('Proxy :: Proxy x) @@ (g @@ ('Proxy :: Proxy x)) | |
dcomp1 f _ _ = f @x @(g @@ ('Proxy :: Proxy x)) | |
#if __GLASGOW_HASKELL__ >= 805 | |
dcomp2 :: forall (a :: Type) | |
(b :: a ~> Type) | |
(c :: forall (x :: a). Proxy x ~> b @@ x ~> Type) | |
(f :: forall (x :: a) (y :: b @@ x). Proxy x ~> Proxy y ~> c @@ ('Proxy :: Proxy x) @@ y) | |
(g :: forall (x :: a). Proxy x ~> b @@ x) | |
(x :: a). | |
SingKind (c @@ ('Proxy :: Proxy x) @@ (g @@ ('Proxy :: Proxy x))) | |
=> (forall (xx :: a) (yy :: b @@ xx). Sing (f @@ ('Proxy :: Proxy xx) @@ ('Proxy :: Proxy yy))) | |
-> (forall (xx :: a). Sing (g @@ ('Proxy :: Proxy xx))) | |
-> Sing x | |
-> Demote (c @@ ('Proxy :: Proxy x) @@ (g @@ ('Proxy :: Proxy x))) | |
dcomp2 sf _ _ = fromSing $ sf @x @(g @@ ('Proxy :: Proxy x)) | |
#endif |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment