F.hs

{-# LANGUAGE
  DataKinds,
  PolyKinds,
  StandaloneKindSignatures,
  TypeFamilies #-}
module F where

import Data.Void
import Data.Functor.Const
import Data.Kind (Type)
import Data.Type.Bool
import GHC.TypeLits
import GHC.TypeNats

type Exp a = Const Void a -> Type

type family Eval (e :: Exp a) :: a

-- | A spine indexed by a heterogeneous list.
type PList :: forall ls. ls -> Type
data PList (ks :: ls) where
  PNil :: PList '()
  (:+) :: () -> PList ks -> PList '(k, ks)

infixr 1 :+

type Family :: forall name -> forall ks. FamilyParams name ks -> FamilyArgs name ks -> Exp (FamilyResult name ks)
data Family (name :: Symbol) (proxy :: FamilyParams name ks)
  :: FamilyArgs name ks -> Exp (FamilyResult name ks)

type FamilyParams (name :: Symbol) (ks :: FamilyParamsKind name) = PList ks

type family FamilyParamsKind (name :: Symbol) :: Type

type FamilyArgs name p = Fst (FamilySig name p)
type FamilyResult name p = Snd (FamilySig name p)
type family FamilySig (name :: Symbol) (ks :: FamilyParamsKind name) :: (Type, Type)

type family Fst (p :: (k, l)) :: k where
  Fst '(x, _) = x

type family Snd (p :: (k, l)) :: l where
  Snd '(_, y) = y

type instance FamilyParamsKind "++" = ()
type instance FamilySig "++" _ = '((Symbol, Symbol), Symbol)
type instance Eval (Family "++" _ '(x, y)) = AppendSymbol x y

type instance FamilyParamsKind "+" = ()
type instance FamilySig "+" _ = '((Nat, Nat), Nat)
type instance Eval (Family "+" _ '(x, y)) = x + y

type instance FamilyParamsKind "If" = (Type, ())
type instance FamilySig "If" '(k, _) = '((Bool, k, k), k)
type instance Eval (Family "If" (_ :+ PNil) '(b, t, f)) = If b t f

-- Look ma', no kinds!
type Example = Family "If" ('() :+ PNil) '( 'True, '[], '[])

foo :: proxy (Eval Example) -> proxy '[]
foo x = x