Copyright	(c) Murdoch J. Gabbay 2020
License	GPL-3
Maintainer	murdoch.gabbay@gmail.com
Stability	experimental
Portability	POSIX
Safe Haskell	None
Language	Haskell2010

Language.Nominal.Examples.SystemF

Contents

Introduction
System F types
System F terms
Normal forms
Pretty-printer
Helper functions for building terms
Example terms
Tests

Description

Syntax and reductions of System F using the Nominal package

Synopsis

data ATrm
data ATyp
type NTypLabel = String
type NTyp = KName ATyp NTypLabel
data Typ
- = TVar NTyp
- | Typ :-> Typ
- | All (KAbs NTyp Typ)
typRecurse :: (NTyp -> a) -> (Typ -> Typ -> a) -> (NTyp -> Typ -> a) -> Typ -> a
type NTrmLabel = (String, Typ)
type NTrm = KName ATrm NTrmLabel
data Trm
- = Var NTrm
- | App Trm Trm
- | Lam (KAbs NTrm Trm)
- | TApp Trm Typ
- | TLam (KAbs NTyp Trm)
typeOf :: Trm -> Maybe Typ
typeOf' :: Trm -> Typ
typeable :: Trm -> Bool
nf :: Trm -> Maybe Trm
nf' :: Trm -> Trm
normalisable :: Trm -> Bool
class PP a where
- ppp :: a -> String
- pp :: a -> IO ()
tall :: NTypLabel -> (Typ -> Typ) -> Typ
tlam :: NTypLabel -> (Typ -> Trm) -> Trm
lam :: NTrmLabel -> (Trm -> Trm) -> Trm
(@.) :: Trm -> Trm -> Trm
(@:) :: Trm -> Typ -> Trm
idTrm :: Trm
idTrm2 :: Trm
zero :: Trm
suc :: Trm
one :: Trm
nat :: Typ
church :: Int -> Trm
transform :: Typ
selfapp :: Trm

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 Methods showsPrec :: Int -> Maybe Typ -> ShowS # show :: Maybe Typ -> String # showList :: [Maybe Typ] -> ShowS #
type Rep Typ Source #
Instance details Defined in Language.Nominal.Examples.SystemF type Rep Typ = D1 (MetaData "Typ" "Language.Nominal.Examples.SystemF" "nom-0.1.0.1-3UtpNOnqRlSC6EhVIia7SR" 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 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 Methods showsPrec :: Int -> Maybe Trm -> ShowS # show :: Maybe Trm -> String # showList :: [Maybe Trm] -> ShowS #
type Rep Trm Source #
Instance details Defined in Language.Nominal.Examples.SystemF type Rep Trm = D1 (MetaData "Trm" "Language.Nominal.Examples.SystemF" "nom-0.1.0.1-3UtpNOnqRlSC6EhVIia7SR" 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 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 #