Type lambdas and induction with GHC 8.4.2 and singletons

TypeLambdas.hs

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

import Data.Singletons.TH -- singletons 2.4.1
import Data.Kind

-- some standard stuff for later examples' sake
--------------------------------------------------------------------------------

singletons([d| data Nat = Z | S Nat |])

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

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

-- Type-level lambdas
--------------------------------------------------------------------------------

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 Apply (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