Skip to content

Instantly share code, notes, and snippets.

@RyanGlScott
Last active Nov 30, 2018
Embed
What would you like to do?
Conor McBride's S combinator in GHC
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE LiberalTypeSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module S where
import Data.Kind
data TyFun :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
infixr 0 ~>
type family (f :: a ~> b) @@ (x :: a) :: b
type KindOf (a :: k) = k
-- | Warm-up.
type DApply a
(b :: a ~> Type)
(f :: KindOf (DApplyAux a b))
-- (f :: forall (x :: a) -> b @@ x)
(x :: a)
= (f x :: b @@ x)
type family DApplyAux a (b :: a ~> Type) (x :: a) :: b @@ x where {}
-- | Conor McBride's S combinator.
type S a
(b :: a ~> Type)
(c :: KindOf (SAux1 a b))
-- (c :: forall (x :: a) -> (b @@ x ~> Type))
(f :: KindOf (SAux2 a b c))
-- (f :: forall (x :: a) (y :: b @@ x) -> c x @@ y)
(g :: KindOf (SAux3 a b))
-- (g :: forall (x :: a) -> b @@ x)
(x :: a)
= (f x (g x) :: c x @@ g x)
type family SAux1 a (b :: a ~> Type)
(x :: a) :: b @@ x ~> Type
type family SAux2 a (b :: a ~> Type) (c :: KindOf (SAux1 a b))
(x :: a) (y :: b @@ x) :: c x @@ y
type SAux3 a (b :: a ~> Type) (x :: a) = (DApplyAux a b x :: b @@ x)
-- | Depedent function composition (in limited form).
type DComp a
(b :: a -> Type)
(c :: forall (x :: a). KindOf (DCompAux1 a b x))
-- (c :: forall (x :: a). b x -> Type)
(f :: forall (x :: a). KindOf (DCompAux2 a b c x))
-- (f :: forall (x :: a). forall (y :: b x) -> c y)
(g :: KindOf (DCompAux3 a b))
-- (g :: forall (x :: a) -> b x)
(x :: a)
= (f (g x) :: c (g x))
type family DCompAux1 a (b :: a -> Type)
(x :: a) :: b x -> Type
type family DCompAux2 a (b :: a -> Type) (c :: forall (x :: a). KindOf (DCompAux1 a b x))
(x :: a) (y :: b x) :: c y
type family DCompAux3 a (b :: a -> Type) (x :: a) :: b x
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment