ThePowerOfDefun.hs

{-# 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