Language.Nominal.Examples.SystemF

Syntax and reductions of System F using the Nominal package

Introduction

System F is a classic example and has some interesting features:

• Two kinds of variable: type variables and term variables.
• Three kinds of binding: type forall binding a type variable in a type; term lambda binding a term variable in a term; and type lambda binding a type variable in a term.
• A static assignment of semantic information to term variables, namely: a type assignment. Thus intuitively term variables carry labels (types), which themselves may contain type variables.
• And it's an expressive system of independent mathematical interest.

So implementing System F is a natural test for this package. We start with atoms:

data ATrm

With DataKinds, we obtain:

• ATyp a type of atoms to identify type variables NTyp, and
• ATrm a type of atoms to identify term variables NTrm.

See Tom for more discussion of how this works.

Instances

Data ATrm

Defined in Language.Nominal.Examples.SystemF

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ATrm -> c ATrm

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ATrm

toConstr :: ATrm -> Constr

dataTypeOf :: ATrm -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ATrm)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ATrm)

gmapT :: (forall b. Data b => b -> b) -> ATrm -> ATrm

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ATrm -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ATrm -> r

gmapQ :: (forall d. Data d => d -> u) -> ATrm -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> ATrm -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ATrm -> m ATrm

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ATrm -> m ATrm

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ATrm -> m ATrm

PP NTrm

Pretty-print term variable

Defined in Language.Nominal.Examples.SystemF

Methods

ppp :: NTrm -> String

pp :: NTrm -> IO ()

KSub NTrm Trm Trm

Substitute term variable with term in term

Defined in Language.Nominal.Examples.SystemF

Methods

sub :: NTrm -> Trm -> Trm -> Trm

KSub NTyp Typ NTrm

Substitute type variables with type in term variable. Non-trivial because a term variable carries a label which contains a type. Action is functorial, descending into the type label.

Defined in Language.Nominal.Examples.SystemF

Methods

sub :: NTyp -> Typ -> NTrm -> NTrm

data ATyp

With DataKinds, we obtain:

• ATyp a type of atoms to identify type variables NTyp, and
• ATrm a type of atoms to identify term variables NTrm.

See Tom for more discussion of how this works.

Instances

Data ATyp

Defined in Language.Nominal.Examples.SystemF

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ATyp -> c ATyp

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ATyp

toConstr :: ATyp -> Constr

dataTypeOf :: ATyp -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ATyp)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ATyp)

gmapT :: (forall b. Data b => b -> b) -> ATyp -> ATyp

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ATyp -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ATyp -> r

gmapQ :: (forall d. Data d => d -> u) -> ATyp -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> ATyp -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ATyp -> m ATyp

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ATyp -> m ATyp

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ATyp -> m ATyp

PP NTyp

Pretty-print type variable

Defined in Language.Nominal.Examples.SystemF

Methods

ppp :: NTyp -> String

pp :: NTyp -> IO ()

KSub NTyp Typ Trm

Defined in Language.Nominal.Examples.SystemF

Methods

sub :: NTyp -> Typ -> Trm -> Trm

KSub NTyp Typ NTrm

Substitute type variables with type in term variable. Non-trivial because a term variable carries a label which contains a type. Action is functorial, descending into the type label.

Defined in Language.Nominal.Examples.SystemF

Methods

sub :: NTyp -> Typ -> NTrm -> NTrm

KSub NTyp Typ Typ

Substitution acts on type variables. Capture-avoidance is automagical.

Defined in Language.Nominal.Examples.SystemF

Methods

sub :: NTyp -> Typ -> Typ -> Typ

System F types

type NTypLabel = String

A type variable is labelled just by a display name

type NTyp = KName ATyp NTypLabel

A type variable name. Internally, this consists of

• an atom of type KAtom ATyp, and
• a label of type NTypLabel, which is just a display name in String.

data Typ

Datatype of System F types

We use Generic to deduce a swapping action for atoms of sorts ATyp and ATrm. Just once, we spell out the definition implicit in the generic instance:

instance Swappable Typ where
   swpN n1 n2 (TVar n)   = TVar $ swpN n1 n2 n
   swpN n1 n2 (t' :-> t) = swpN n1 n2 t' :-> swpN n1 n2 t
   swpN n1 n2 (All x)    = All $ swpN n1 n2 x

This is boring, and automated, and that's the point: swappings distribute uniformly through everything including abstractors (the x under the All).

(The mathematical reason for this is that swappings are invertible, whereas renamings and substitutions aren't.)

Constructors

TVar NTyp

Type variable

Typ :-> Typ

Type application

All (KAbs NTyp Typ)

Type forall-abstraction

Instances

Eq Typ

Defined in Language.Nominal.Examples.SystemF

Methods

(==) :: Typ -> Typ -> Bool

(/=) :: Typ -> Typ -> Bool

Data Typ

Defined in Language.Nominal.Examples.SystemF

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Typ -> c Typ

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Typ

toConstr :: Typ -> Constr

dataTypeOf :: Typ -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Typ)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Typ)

gmapT :: (forall b. Data b => b -> b) -> Typ -> Typ

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Typ -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Typ -> r

gmapQ :: (forall d. Data d => d -> u) -> Typ -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Typ -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Typ -> m Typ

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Typ -> m Typ

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Typ -> m Typ

Show Typ

Defined in Language.Nominal.Examples.SystemF

Methods

showsPrec :: Int -> Typ -> ShowS

show :: Typ -> String

showList :: [Typ] -> ShowS

Generic Typ

Defined in Language.Nominal.Examples.SystemF

Associated Types

type Rep Typ :: Type -> Type

Methods

from :: Typ -> Rep Typ x

to :: Rep Typ x -> Typ

Arbitrary Typ

For QuickCheck tests: pick a type

Defined in Language.Nominal.Properties.SpecUtilities

Methods

arbitrary :: Gen Typ

shrink :: Typ -> [Typ]

Swappable Typ

Defined in Language.Nominal.Examples.SystemF

Methods

kswp :: Typeable s => KAtom s -> KAtom s -> Typ -> Typ

PP NTrm

Pretty-print term variable

Defined in Language.Nominal.Examples.SystemF

Methods

ppp :: NTrm -> String

pp :: NTrm -> IO ()

PP Typ

Pretty-print type

Defined in Language.Nominal.Examples.SystemF

Methods

ppp :: Typ -> String

pp :: Typ -> IO ()

KSub NTrm Trm Trm

Substitute term variable with term in term

Defined in Language.Nominal.Examples.SystemF

Methods

sub :: NTrm -> Trm -> Trm -> Trm

KSub NTyp Typ Trm

Defined in Language.Nominal.Examples.SystemF

Methods

sub :: NTyp -> Typ -> Trm -> Trm

KSub NTyp Typ NTrm

Substitute type variables with type in term variable. Non-trivial because a term variable carries a label which contains a type. Action is functorial, descending into the type label.

Defined in Language.Nominal.Examples.SystemF

Methods

sub :: NTyp -> Typ -> NTrm -> NTrm

KSub NTyp Typ Typ

Substitution acts on type variables. Capture-avoidance is automagical.

Defined in Language.Nominal.Examples.SystemF

Methods

sub :: NTyp -> Typ -> Typ -> Typ

Show (Maybe Typ)

Defined in Language.Nominal.Examples.SystemF

Methods

showsPrec :: Int -> Maybe Typ -> ShowS

show :: Maybe Typ -> String

showList :: [Maybe Typ] -> ShowS

type Rep Typ

Defined in Language.Nominal.Examples.SystemF

type Rep Typ = D1 (MetaData "Typ" "Language.Nominal.Examples.SystemF" "nom-0.1.0.2-Cei0dwnsIrWHLKrPA11A4S" False) (C1 (MetaCons "TVar" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 NTyp)) :+: (C1 (MetaCons ":->" (InfixI LeftAssociative 9) False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Typ) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Typ)) :+: C1 (MetaCons "All" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (KAbs NTyp Typ)))))

typRecurse :: (NTyp -> a) -> (Typ -> Typ -> a) -> (NTyp -> Typ -> a) -> Typ -> a

Nominal recursion scheme. We never use it because it's implicit in pattern-matching. See e.g. code for typeOf, nf, and ppp.

System F terms

type NTrmLabel = (String, Typ)

A term variable is labelled by a display name, and its type

type NTrm = KName ATrm NTrmLabel

A term variable name

data Trm

System F terms.

• We get swapping actions automatically, and also substitution of type names NTyp for types Typ.
• Substitution of term variables NTrm for terms Trm needs defined separately.

Constructors

Var NTrm

Term variable, labelled by its display name and type

App Trm Trm

Apply a term to a term

Lam (KAbs NTrm Trm)

Nominal atoms-abstraction by a term variable.

TApp Trm Typ

Apply a term to a type

TLam (KAbs NTyp Trm)

Nominal atoms-abstraction by a type variable.

Instances

Eq Trm

Defined in Language.Nominal.Examples.SystemF

Methods

(==) :: Trm -> Trm -> Bool

(/=) :: Trm -> Trm -> Bool

Data Trm

Defined in Language.Nominal.Examples.SystemF

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Trm -> c Trm

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Trm

toConstr :: Trm -> Constr

dataTypeOf :: Trm -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Trm)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Trm)

gmapT :: (forall b. Data b => b -> b) -> Trm -> Trm

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Trm -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Trm -> r

gmapQ :: (forall d. Data d => d -> u) -> Trm -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Trm -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Trm -> m Trm

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Trm -> m Trm

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Trm -> m Trm

Show Trm

Defined in Language.Nominal.Examples.SystemF

Methods

showsPrec :: Int -> Trm -> ShowS

show :: Trm -> String

showList :: [Trm] -> ShowS

Generic Trm

Defined in Language.Nominal.Examples.SystemF

Associated Types

type Rep Trm :: Type -> Type

Methods

from :: Trm -> Rep Trm x

to :: Rep Trm x -> Trm

Arbitrary Trm

For QuickCheck tests: pick a term

Defined in Language.Nominal.Properties.SpecUtilities

Methods

arbitrary :: Gen Trm

shrink :: Trm -> [Trm]

Swappable Trm

Defined in Language.Nominal.Examples.SystemF

Methods

kswp :: Typeable s => KAtom s -> KAtom s -> Trm -> Trm

PP Trm

Pretty-print term

Defined in Language.Nominal.Examples.SystemF

Methods

ppp :: Trm -> String

pp :: Trm -> IO ()

KSub NTrm Trm Trm

Substitute term variable with term in term

Defined in Language.Nominal.Examples.SystemF

Methods

sub :: NTrm -> Trm -> Trm -> Trm

KSub NTyp Typ Trm

Defined in Language.Nominal.Examples.SystemF

Methods

sub :: NTyp -> Typ -> Trm -> Trm

Show (Maybe Trm)

Defined in Language.Nominal.Examples.SystemF

Methods

showsPrec :: Int -> Maybe Trm -> ShowS

show :: Maybe Trm -> String

showList :: [Maybe Trm] -> ShowS

type Rep Trm

Defined in Language.Nominal.Examples.SystemF

type Rep Trm = D1 (MetaData "Trm" "Language.Nominal.Examples.SystemF" "nom-0.1.0.2-Cei0dwnsIrWHLKrPA11A4S" False) ((C1 (MetaCons "Var" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 NTrm)) :+: C1 (MetaCons "App" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Trm) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Trm))) :+: (C1 (MetaCons "Lam" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (KAbs NTrm Trm))) :+: (C1 (MetaCons "TApp" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Trm) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Typ)) :+: C1 (MetaCons "TLam" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (KAbs NTyp Trm))))))

typeOf :: Trm -> Maybe Typ

Calculate type of term, maybe

typeOf' :: Trm -> Typ

Calculate type of term; raise error if none exists

typeable :: Trm -> Bool

True if term is typeable; False if not.

Normal forms

nf :: Trm -> Maybe Trm

Normal form, maybe

nf' :: Trm -> Trm

Normal form; raise error if none

normalisable :: Trm -> Bool

True if term is normalisable; false if not.

Pretty-printer

class PP a where

Typeclass for things that can be pretty-printed

Minimal complete definition

ppp

Methods

ppp :: a -> String

pp :: a -> IO ()

Instances

PP Trm

Pretty-print term

Defined in Language.Nominal.Examples.SystemF

Methods

ppp :: Trm -> String

pp :: Trm -> IO ()

PP NTrm

Pretty-print term variable

Defined in Language.Nominal.Examples.SystemF

Methods

ppp :: NTrm -> String

pp :: NTrm -> IO ()

PP Typ

Pretty-print type

Defined in Language.Nominal.Examples.SystemF

Methods

ppp :: Typ -> String

pp :: Typ -> IO ()

PP NTyp

Pretty-print type variable

Defined in Language.Nominal.Examples.SystemF

Methods

ppp :: NTyp -> String

pp :: NTyp -> IO ()

Helper functions for building terms

tall :: NTypLabel -> (Typ -> Typ) -> Typ

Build type quantification from function: f ↦ ∀ a.(f a) for fresh a

tlam :: NTypLabel -> (Typ -> Trm) -> Trm

Build type lambda from function: f ↦ Λ a.(f a) for fresh a

lam :: NTrmLabel -> (Trm -> Trm) -> Trm

Build term lambda from function: f ↦ λ a.(f a) for fresh a

(@.) :: Trm -> Trm -> Trm

Term-to-term application

(@:) :: Trm -> Typ -> Trm

Term-to-type application

Example terms

idTrm :: Trm

polymorphic identity term = λX x:X.x

idTrm2 :: Trm

Another rendering of polymorphic identity term

zero :: Trm

0 = λX λs:X->X λz:X.z

suc :: Trm

suc = λx:(∀X.(X->X)->X->X) X s:X->X z:X.s(n[X] s z)

one :: Trm

1

nat :: Typ

nat

church :: Int -> Trm

Cast an Int to the corresponding Church numeral.

transform :: Typ

Transformer type = ∀X.X->X

selfapp :: Trm

Self-application = λx:∀X.X->X.x[∀X.X->X] x

Tests

Property-based tests are in Language.Nominal.Properties.Examples.SystemFSpec.