System F

SystemF.hs

-- SYSTEM F
--   http://homepages.inf.ed.ac.uk/slindley/papers/embedding-f.pdf
-- 
-- Type-level lambdas
--   https://gist.github.com/AndrasKovacs/ac71371d0ca6e0995541e42cd3a3b0cf


{-# 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 = V VZ
type V1 = V (VS VZ)
type V2 = V (VS (VS VZ))
type V3 = V (VS (VS (VS VZ)))
type V4 = V (VS (VS (VS (VS VZ))))

-- 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 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 V0 (T a) :-> T2 Vec 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 V0 (T a) :-> T2 Vec V0 (T b) :-> T2 Vec V0 (T c)))
    (\_ _ -> Nil)
    (\hyp (a :> as) (b :> bs) -> f a b :> hyp as bs)
    (sing @_ @n) as bs

type a --> b = Term '[] (a ~> b)

type exp · a = Eval exp @@ a

newtype Poly :: (Type --> Type) -> Type where
  Poly :: (forall xx. lam · xx) 
       -> Poly lam

data Exp :: [Type] -> Type -> Type where
  Var :: Var as a -> Exp as a

  Lam :: Exp (a:as) b -> Exp as (a -> b)

  App :: Exp as (a -> b) -> (Exp as a -> Exp as b)

  TLam :: (forall xx. Exp as (lam · xx)) -> Exp as (Poly lam)

  TApp :: Exp as (Poly lam) -> Exp as (lam · xx)

type AtoA = L (V0 :-> V0)

type Closed = Exp '[]

--      :: Closed (Poly (\a -> a -> a))
id_poly :: Closed (Poly AtoA)
id_poly = TLam (Lam (Var VZ))

id_int :: Closed (Int -> Int)
id_int = TApp id_poly

This is a direct combination of

Embedding F

and

AndrasKovacs's type-level lambdas