nom-0.1.0.1: Name-binding & alpha-equivalence

Copyright(c) Murdoch J. Gabbay 2020
LicenseGPL-3
Maintainermurdoch.gabbay@gmail.com
Stabilityexperimental
PortabilityPOSIX
Safe HaskellNone
LanguageHaskell2010

Language.Nominal.Examples.SystemF

Contents

Description

Syntax and reductions of System F using the Nominal package

Synopsis

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 Source #

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 Source # 
Instance details

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 Source #

Pretty-print term variable

Instance details

Defined in Language.Nominal.Examples.SystemF

Methods

ppp :: NTrm -> String Source #

pp :: NTrm -> IO () Source #

KSub NTrm Trm Trm Source #

Substitute term variable with term in term

Instance details

Defined in Language.Nominal.Examples.SystemF

Methods

sub :: NTrm -> Trm -> Trm -> Trm Source #

KSub NTyp Typ NTrm Source #

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.

Instance details

Defined in Language.Nominal.Examples.SystemF

Methods

sub :: NTyp -> Typ -> NTrm -> NTrm Source #

data ATyp Source #

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 Source # 
Instance details

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 Source #

Pretty-print type variable

Instance details

Defined in Language.Nominal.Examples.SystemF

Methods

ppp :: NTyp -> String Source #

pp :: NTyp -> IO () Source #

KSub NTyp Typ Trm Source # 
Instance details

Defined in Language.Nominal.Examples.SystemF

Methods

sub :: NTyp -> Typ -> Trm -> Trm Source #

KSub NTyp Typ NTrm Source #

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.

Instance details

Defined in Language.Nominal.Examples.SystemF

Methods

sub :: NTyp -> Typ -> NTrm -> NTrm Source #

KSub NTyp Typ Typ Source #

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

Instance details

Defined in Language.Nominal.Examples.SystemF

Methods

sub :: NTyp -> Typ -> Typ -> Typ Source #

System F types

type NTypLabel = String Source #

A type variable is labelled just by a display name

type NTyp = KName ATyp NTypLabel Source #

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 Source #

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 Source # 
Instance details

Defined in Language.Nominal.Examples.SystemF

Methods

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

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

Data Typ Source # 
Instance details

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 Source # 
Instance details

Defined in Language.Nominal.Examples.SystemF

Methods

showsPrec :: Int -> Typ -> ShowS #

show :: Typ -> String #

showList :: [Typ] -> ShowS #

Generic Typ Source # 
Instance details

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 Source #

For QuickCheck tests: pick a type

Instance details

Defined in Language.Nominal.Properties.SpecUtilities

Methods

arbitrary :: Gen Typ #

shrink :: Typ -> [Typ] #

Swappable Typ Source # 
Instance details

Defined in Language.Nominal.Examples.SystemF

Methods

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

PP NTrm Source #

Pretty-print term variable

Instance details

Defined in Language.Nominal.Examples.SystemF

Methods

ppp :: NTrm -> String Source #

pp :: NTrm -> IO () Source #

PP Typ Source #

Pretty-print type

Instance details

Defined in Language.Nominal.Examples.SystemF

Methods

ppp :: Typ -> String Source #

pp :: Typ -> IO () Source #

KSub NTrm Trm Trm Source #

Substitute term variable with term in term

Instance details

Defined in Language.Nominal.Examples.SystemF

Methods

sub :: NTrm -> Trm -> Trm -> Trm Source #

KSub NTyp Typ Trm Source # 
Instance details

Defined in Language.Nominal.Examples.SystemF

Methods

sub :: NTyp -> Typ -> Trm -> Trm Source #

KSub NTyp Typ NTrm Source #

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.

Instance details

Defined in Language.Nominal.Examples.SystemF

Methods

sub :: NTyp -> Typ -> NTrm -> NTrm Source #

KSub NTyp Typ Typ Source #

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

Instance details

Defined in Language.Nominal.Examples.SystemF

Methods

sub :: NTyp -> Typ -> Typ -> Typ Source #

Show (Maybe Typ) Source # 
Instance details

Defined in Language.Nominal.Examples.SystemF

type Rep Typ Source # 
Instance details

Defined in Language.Nominal.Examples.SystemF

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

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) Source #

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

type NTrm = KName ATrm NTrmLabel Source #

A term variable name

data Trm Source #

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 Source # 
Instance details

Defined in Language.Nominal.Examples.SystemF

Methods

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

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

Data Trm Source # 
Instance details

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 Source # 
Instance details

Defined in Language.Nominal.Examples.SystemF

Methods

showsPrec :: Int -> Trm -> ShowS #

show :: Trm -> String #

showList :: [Trm] -> ShowS #

Generic Trm Source # 
Instance details

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 Source #

For QuickCheck tests: pick a term

Instance details

Defined in Language.Nominal.Properties.SpecUtilities

Methods

arbitrary :: Gen Trm #

shrink :: Trm -> [Trm] #

Swappable Trm Source # 
Instance details

Defined in Language.Nominal.Examples.SystemF

Methods

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

PP Trm Source #

Pretty-print term

Instance details

Defined in Language.Nominal.Examples.SystemF

Methods

ppp :: Trm -> String Source #

pp :: Trm -> IO () Source #

KSub NTrm Trm Trm Source #

Substitute term variable with term in term

Instance details

Defined in Language.Nominal.Examples.SystemF

Methods

sub :: NTrm -> Trm -> Trm -> Trm Source #

KSub NTyp Typ Trm Source # 
Instance details

Defined in Language.Nominal.Examples.SystemF

Methods

sub :: NTyp -> Typ -> Trm -> Trm Source #

Show (Maybe Trm) Source # 
Instance details

Defined in Language.Nominal.Examples.SystemF

type Rep Trm Source # 
Instance details

Defined in Language.Nominal.Examples.SystemF

typeOf :: Trm -> Maybe Typ Source #

Calculate type of term, maybe

typeOf' :: Trm -> Typ Source #

Calculate type of term; raise error if none exists

typeable :: Trm -> Bool Source #

True if term is typeable; False if not.

Normal forms

nf :: Trm -> Maybe Trm Source #

Normal form, maybe

nf' :: Trm -> Trm Source #

Normal form; raise error if none

normalisable :: Trm -> Bool Source #

True if term is normalisable; false if not.

Pretty-printer

class PP a where Source #

Typeclass for things that can be pretty-printed

Minimal complete definition

ppp

Methods

ppp :: a -> String Source #

pp :: a -> IO () Source #

Instances
PP Trm Source #

Pretty-print term

Instance details

Defined in Language.Nominal.Examples.SystemF

Methods

ppp :: Trm -> String Source #

pp :: Trm -> IO () Source #

PP NTrm Source #

Pretty-print term variable

Instance details

Defined in Language.Nominal.Examples.SystemF

Methods

ppp :: NTrm -> String Source #

pp :: NTrm -> IO () Source #

PP Typ Source #

Pretty-print type

Instance details

Defined in Language.Nominal.Examples.SystemF

Methods

ppp :: Typ -> String Source #

pp :: Typ -> IO () Source #

PP NTyp Source #

Pretty-print type variable

Instance details

Defined in Language.Nominal.Examples.SystemF

Methods

ppp :: NTyp -> String Source #

pp :: NTyp -> IO () Source #

Helper functions for building terms

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

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

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

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

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

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

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

Term-to-term application

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

Term-to-type application

Example terms

idTrm :: Trm Source #

polymorphic identity term = λX x:X.x

idTrm2 :: Trm Source #

Another rendering of polymorphic identity term

zero :: Trm Source #

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

suc :: Trm Source #

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

nat :: Typ Source #

nat

church :: Int -> Trm Source #

Cast an Int to the corresponding Church numeral.

transform :: Typ Source #

Transformer type = ∀X.X->X

selfapp :: Trm Source #

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

Tests