Type lambdas without singletons dependency

TypeLambdasNoSingletons.hs

{-# language ScopedTypeVariables, RankNTypes, TypeFamilies,
             UndecidableInstances, GADTs, TypeOperators,
             TypeApplications, AllowAmbiguousTypes, TypeInType,
             StandaloneDeriving #-}

import Data.Kind

-- singletons
--------------------------------------------------------------------------------

data family Sing (t :: a)

class SingI (t :: a) where sing :: Sing t

data TyFun (a :: Type) (b :: Type)
type a ~> b = TyFun a b -> Type
infixr 0 ~>

type family (@@) (f :: a ~> b) (x :: a) :: b
infixl 9 @@

data TyCon1 :: (a -> b) -> a ~> b
data TyCon2 :: (a -> b -> c) -> a ~> b ~> c
data TyCon3 :: (a -> b -> c -> d) -> a ~> b ~> c ~> d
data TyCon4 :: (a -> b -> c -> d -> e) -> a ~> b ~> c ~> d ~> e
type instance (TyCon1 f) @@ x = f x
type instance (TyCon2 f) @@ x = TyCon1 (f x)
type instance (TyCon3 f) @@ x = TyCon2 (f x)
type instance (TyCon4 f) @@ x = TyCon3 (f x)

--------------------------------------------------------------------------------

data Nat = Z | S Nat
data instance Sing (n :: Nat) where
  SZ :: Sing Z
  SS :: Sing n -> Sing (S n)

instance SingI Z where sing = SZ
instance SingI n => SingI (S n) where sing = SS sing

data Vec n a where
  Nil  :: Vec Z a
  (:>) :: a -> Vec n a -> Vec (S n) a
infixr 5 :>

deriving instance Show a => Show (Vec n a)

--------------------------------------------------------------------------------

data Var :: [Type] -> Type -> Type where
  VZ :: Var (t ': ts) t
  VS :: Var ts t -> Var (t' ': ts) t

data Term :: [Type] -> Type -> Type where
  T    :: t -> Term ts t
  V    :: Var ts t -> Term ts t                      -- Var
  L    :: Term (t ': ts) t' -> Term ts (t ~> t')     -- Lam
  (:$) :: Term ts (a ~> b) -> Term ts a -> Term ts b -- App

infixl 9 :$

data Env :: [Type] -> Type where
  ENil  :: Env '[]
  ECons :: t -> Env cxt -> Env (t ': cxt)

type family LookupVar (v :: Var cxt t) (env :: Env cxt) :: t where
  LookupVar VZ     (ECons x env) = x
  LookupVar (VS v) (ECons x env) = LookupVar v env

type family Eval (term :: Term '[] t) :: t where
  Eval term = Eval_ term ENil

type family Eval_ (term :: Term cxt t) (env :: Env cxt) :: t where
  Eval_ (T x)       env = x
  Eval_ (V v)       env = LookupVar v env
  Eval_ (f :$ x)    env = Eval_ f env @@ Eval_ x env
  Eval_ (L e)       env = LamS e env

data LamS :: Term (a ': cxt) b -> Env cxt -> a ~> b
type instance (LamS e env) @@ x = Eval_ e (ECons x env)

-- shorthands for variables
type V0 = VZ
type V1 = VS V0
type V2 = VS V1
type V3 = VS V2
type V4 = VS V3

-- term shorthand for (->)
type (:->) a b = (T (TyCon2 (->))) :$ a :$ b
infixr 0 :->

-- shorthands for type constructors
type T1 f a = T (TyCon1 f) :$ a
type T2 f a b = T (TyCon2 f) :$ a :$ b
type T3 f a b c = T (TyCon3 f) :$ a :$ b :$ c
type T4 f a b c d  = T (TyCon4 f) :$ a :$ b :$ c :$ d

-- infix type family application, meant for L (type lambda)
-- like "L$ L$ L$ ..."
infixr 0 $
type ($) f x = f x

-- Induction for Nat
--------------------------------------------------------------------------------

natIndS ::
  forall p n. p @@ Z -> (forall n. Sing n -> p @@ n -> p @@ S n) -> forall n. Sing n -> p @@ n
natIndS z s SZ      = z
natIndS z s (SS sn) = s sn (natIndS @p z s sn)

natInd ::
  forall p n. p @@ Z -> (forall n. p @@ n -> p @@ S n) -> forall n. Sing n -> p @@ n
natInd z s = natIndS @p z (\(sn :: Sing n') pn -> s @n' pn)

-- Examples using induction and type lambdas
--------------------------------------------------------------------------------

vReplicate :: forall a n. Sing n -> a -> Vec n a
vReplicate n a =
  -- natInd (\n -> Vec n a) ...
  natInd @(Eval (L$ T2 Vec (V V0) (T a))) Nil (a :>) n

vFmap :: forall a b n. SingI n => (a -> b) -> Vec n a -> Vec n b
vFmap f as =
  -- natInd (\n -> Vec n a -> Vec n b) ...
  natInd
    @(Eval (L$ T2 Vec (V V0) (T a) :-> T2 Vec (V V0) (T b)))
    (\_ -> Nil) (\hyp (a :> as) -> f a :> hyp as) (sing @_ @n) as

vZipWith :: forall a b c n. SingI n => (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
vZipWith f as bs =
  -- natInd (\n -> Vec n a -> Vec n b -> Vec n c)
  natInd
    @(Eval (L$ T2 Vec (V V0) (T a) :-> T2 Vec (V V0) (T b) :-> T2 Vec (V V0) (T c)))
    (\_ _ -> Nil)
    (\hyp (a :> as) (b :> bs) -> f a b :> hyp as bs)
    (sing @_ @n) as bs