Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
-- Requires GHC 8.10 or later
module ThePowerOfDefun where
import Data.Kind
import Data.Type.Equality
-----
-- Eliminators
-----
-- type ElimList :: forall (p :: [a] ~> Type) (l :: [a])
-- ~> p @@ '[]
-- ~> (forall (x :: a) (xs :: [a]) -> p @@ xs ~> p @@ (x:xs))
-- ~> p @@ l
type family ElimList
(p :: [a] ~> Type)
(l :: [a])
(pNil :: p @@ '[])
(pCons :: forall (x :: a) (xs :: [a]) -> p @@ xs ~> p @@ (x:xs))
:: p @@ l where
forall a (p :: [a] ~> Type)
(pNil :: p @@ '[])
(pCons :: forall (x :: a) (xs :: [a]) -> p @@ xs ~> p @@ (x:xs)).
ElimList p '[] pNil pCons = pNil
forall a (p :: [a] ~> Type)
(pNil :: p @@ '[])
(pCons :: forall (x :: a) (xs :: [a]) -> p @@ xs ~> p @@ (x:xs))
(x :: a) (xs :: [a]).
ElimList p (x:xs) pNil pCons = pCons x xs @@ ElimList p xs pNil pCons
-- type Wat :: (a ~> b ~> b) ~> (a ~> [a] ~> b ~> b)
type family Wat (f :: a ~> b ~> b) (x :: a) (xs :: [a]) (r :: b) :: b where
Wat f x _ r = f @@ x @@ r
data WatSym0 :: forall a b. (a ~> b ~> b) ~> a ~> [a] ~> b ~> b
data WatSym1 :: forall a b. (a ~> b ~> b) -> a ~> [a] ~> b ~> b
data WatSym2 :: forall a b. (a ~> b ~> b) -> forall (x :: a) -> [a] ~> b ~> b
data WatSym3 :: forall a b. (a ~> b ~> b) -> forall (x :: a) (xs :: [a]) -> b ~> b
type instance Apply WatSym0 f = WatSym1 f
type instance Apply (WatSym1 f) x = WatSym2 f x
type instance Apply (WatSym2 f x) xs = WatSym3 f x xs
type instance Apply (WatSym3 f x xs) r = Wat f x xs r
-- type Foldr :: (a ~> b ~> b) ~> b ~> [a] ~> b
type family Foldr (f :: a ~> b ~> b) (z :: b) (l :: [a]) :: b where
Foldr f (z :: b) l = ElimList (ConstSym1 b) l z (WatSym3 f)
-- type ElimMaybe :: forall (p :: Maybe a ~> Type) (m :: Maybe a)
-- ~> p @@ Nothing
-- ~> (forall (x :: a) -> p @@ Just x)
-- ~> p @@ m
type family ElimMaybe
(p :: Maybe a ~> Type)
(m :: Maybe a)
(pNothing :: p @@ Nothing)
(pJust :: forall (x :: a) -> p @@ Just x) :: p @@ m where
forall a (p :: Maybe a ~> Type)
(pNothing :: p @@ Nothing)
(pJust :: forall (x :: a) -> p @@ Just x).
ElimMaybe p Nothing pNothing pJust = pNothing
forall a (p :: Maybe a ~> Type)
(pNothing :: p @@ Nothing)
(pJust :: forall (x :: a) -> p @@ Just x)
(x :: a).
ElimMaybe p (Just x) pNothing pJust = pJust x
data family Lol :: (a ~> b) -> forall (x :: a) -> b
-- type Unlol :: k ~> k
type family Unlol (a :: k) :: k where
Unlol (Lol f x) = f @@ x
Unlol a = a
-- type ElimMaybeSimple :: Maybe a ~> b ~> (a ~> b) ~> b
type family ElimMaybeSimple (m :: Maybe a) (n :: b) (j :: a ~> b) :: b where
ElimMaybeSimple m (n :: b) j = Unlol (ElimMaybe (ConstSym1 b) m n (Lol j))
-----
-- Examples
-----
-- type Id :: a ~> a
type family Id (x :: a) :: a where
Id x = x
data IdSym0 :: forall a. a ~> a
type instance Apply IdSym0 x = Id x
-- type Const :: a ~> b ~> a
type family Const (x :: a) (y :: b) :: a where
Const x _ = x
data ConstSym0 :: forall a b. a ~> b ~> a
data ConstSym1 :: forall a b. a -> b ~> a
type instance Apply ConstSym0 x = ConstSym1 x
type instance Apply (ConstSym1 x) y = Const x y
type Ex1 = Foldr ConstSym0 0 '[1,2,3]
type Ex2 = Foldr (ConstSym1 IdSym0) 0 '[1,2,3]
type Ex3 = ElimMaybeSimple Nothing "a" IdSym0
type Ex4 = ElimMaybeSimple (Just "b") "a" IdSym0
ex1 :: Ex1 :~: 1
ex1 = Refl
ex2 :: Ex2 :~: 0
ex2 = Refl
ex3 :: Ex3 :~: "a"
ex3 = Refl
ex4 :: Ex4 :~: "b"
ex4 = Refl
-----
-- (~>)
-----
data TyFun :: Type -> Type -> Type
type a ~> b = TyFun a b -> Type
infixr 0 ~>
type family Apply (f :: a ~> b) (x :: a) :: b
type f @@ x = Apply f x
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment