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.Abs

Contents

Description

Name-abstraction, nominal style. This captures the "a." in "λa.ab".

Examples of practical usage are in Language.Nominal.Examples.SystemF, e.g. the type and term datatypes Typ and Trm.

Synopsis

Name-abstraction

data KAbs n a Source #

A datatype for name-abstractions.

  • KAbs n a is a type for abstractions of as by n-names, where we intend that n = KName s t for some s-atoms (atoms of type s) and t-labels (labels of type t).
  • Abs t a is a type for abstractions of as by t-labelled Tom-atoms.

Under the hood an abstraction is just an element of (n, n -> a), but we do not expose this. What makes the type interesting is its constructor, abst :: KName s t -> a -> KAbs (KName s t) a, which is the only way to build an abstraction.

It's possible to implement KAbs using KNom — see absToNom and nomToAbs — but this requires a KSwappable typeclass constraint on a, which we prefer to avoid so that e.g. KAbs can be a Functor.

Instances
(KSupport s a, KSupport s t) => KSupport s (KAbs (KName s t) a) Source #

Support of a :@> x is the support of x minus a

Instance details

Defined in Language.Nominal.Abs

Methods

ksupp :: proxy s -> KAbs (KName s t) a -> Set (KAtom s) Source #

(Typeable s, KUnifyPerm s t, KUnifyPerm s a) => KUnifyPerm s (KAbs (KName s t) a) Source #

Unify Abs name-abstraction

Instance details

Defined in Language.Nominal.Unify

Methods

kunifyPerm :: proxy s -> KAbs (KName s t) a -> KAbs (KName s t) a -> KRen s Source #

ren :: KRen s -> KAbs (KName s t) a -> KAbs (KName s t) a Source #

Functor (KAbs n) Source # 
Instance details

Defined in Language.Nominal.Abs

Methods

fmap :: (a -> b) -> KAbs n a -> KAbs n b #

(<$) :: a -> KAbs n b -> KAbs n a #

Default t => Applicative (KAbs (KName s t)) Source # 
Instance details

Defined in Language.Nominal.Abs

Methods

pure :: a -> KAbs (KName s t) a #

(<*>) :: KAbs (KName s t) (a -> b) -> KAbs (KName s t) a -> KAbs (KName s t) b #

liftA2 :: (a -> b -> c) -> KAbs (KName s t) a -> KAbs (KName s t) b -> KAbs (KName s t) c #

(*>) :: KAbs (KName s t) a -> KAbs (KName s t) b -> KAbs (KName s t) b #

(<*) :: KAbs (KName s t) a -> KAbs (KName s t) b -> KAbs (KName s t) a #

(Typeable s, Swappable t, Eq t, Eq a) => Eq (KAbs (KName s t) a) Source #

Abstractions are equal up to fusing their abstracted names.

Instance details

Defined in Language.Nominal.Abs

Methods

(==) :: KAbs (KName s t) a -> KAbs (KName s t) a -> Bool #

(/=) :: KAbs (KName s t) a -> KAbs (KName s t) a -> Bool #

(Typeable s, Swappable t, Swappable a, Show t, Show a) => Show (KAbs (KName s t) a) Source #

We show an abstraction by evaluating the function inside Abs on a fresh name (with the default Nothing label)

Instance details

Defined in Language.Nominal.Abs

Methods

showsPrec :: Int -> KAbs (KName s t) a -> ShowS #

show :: KAbs (KName s t) a -> String #

showList :: [KAbs (KName s t) a] -> ShowS #

Generic (KAbs n a) Source # 
Instance details

Defined in Language.Nominal.Abs

Associated Types

type Rep (KAbs n a) :: Type -> Type #

Methods

from :: KAbs n a -> Rep (KAbs n a) x #

to :: Rep (KAbs n a) x -> KAbs n a #

(Typeable s, Swappable t, Swappable a, Arbitrary (KName s t), Arbitrary a) => Arbitrary (KAbs (KName s t) a) Source # 
Instance details

Defined in Language.Nominal.Properties.SpecUtilities

Methods

arbitrary :: Gen (KAbs (KName s t) a) #

shrink :: KAbs (KName s t) a -> [KAbs (KName s t) a] #

(Swappable n, Swappable a) => Swappable (KAbs n a) Source #

Spelling out the generic swapping action for clarity, where we write KA for the (internal) constructor for KAbs: kswp n1 n2 (KA n f) = KA (kswp n1 n2 n) (kswp n1 n2 f)

Instance details

Defined in Language.Nominal.Abs

Methods

kswp :: Typeable s => KAtom s -> KAtom s -> KAbs n a -> KAbs n a Source #

Binder (KAbs n a) n a s => BinderConc (KAbs n a) n a s n Source #

Concretes an abstraction at a particular name. Unsafe if the name is not fresh.

(abst a x) `conc` a == x
abst a (x `conc` a) == x -- provided a is suitably fresh. 
new' $ \a -> abst a (x `conc` a) == x  
Instance details

Defined in Language.Nominal.Abs

Methods

conc :: KAbs n a -> n -> a Source #

cnoc :: n -> KAbs n a -> a Source #

(Typeable s, Typeable u, KSub (KName s n) x t, KSub (KName s n) x y, Swappable t, Swappable y) => KSub (KName s n) x (KAbs (KName u t) y) Source #

sub on a nominal abstraction substitutes in the label, and substitutes capture-avoidingly in the body

Instance details

Defined in Language.Nominal.Sub

Methods

sub :: KName s n -> x -> KAbs (KName u t) y -> KAbs (KName u t) y Source #

(Typeable s, Swappable t, Swappable a) => Binder (KAbs (KName s t) a) (KName s t) a s Source #

Acts on an abstraction x' by unpacking x' as (n,x) for a fresh name n, and calculating f n x.

Instance details

Defined in Language.Nominal.Abs

Methods

(@@) :: KAbs (KName s t) a -> (KName s t -> a -> b) -> KNom s b Source #

(@>) :: KName s t -> a -> KAbs (KName s t) a Source #

resMay :: KName s t -> a -> Maybe (KAbs (KName s t) a) Source #

(Typeable s, Swappable n, Swappable x, Swappable y, KSub (KName s n) x y) => BinderConc (KAbs (KName s n) y) (KName s n) y s x Source #

Nameless form of substitution, where the name for which we substitute is packaged in a KAbs abstraction.

Instance details

Defined in Language.Nominal.Sub

Methods

conc :: KAbs (KName s n) y -> x -> y Source #

cnoc :: x -> KAbs (KName s n) y -> y Source #

type Rep (KAbs n a) Source # 
Instance details

Defined in Language.Nominal.Abs

type Rep (KAbs n a) = D1 (MetaData "KAbs" "Language.Nominal.Abs" "nom-0.1.0.1-3UtpNOnqRlSC6EhVIia7SR" False) (C1 (MetaCons "AbsWrapper" PrefixI True) (S1 (MetaSel (Just "absName") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 n) :*: S1 (MetaSel (Just "absApp") NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (n -> a))))

type Abs t a = KAbs (KName Tom t) a Source #

Abstraction by Tom-names.

Abstractions (basic functions)

abst :: (Typeable s, Swappable t, Swappable a) => KName s t -> a -> KAbs (KName s t) a Source #

Create an abstraction by providing a name and a datum in which that name can be swapped (straight out of the paper; publisher and author's pdfs).

Instance of @>, for the case of a nominal abstraction.

abst' :: (Typeable s, Swappable t, Swappable a) => t -> KAtom s -> a -> KAbs (KName s t) a Source #

A KName is just a pair of a label and an KAtom. This version of abst that takes a label and an atom, instead of a name.

pattern (:@>) :: (Typeable s, Swappable t, Swappable a) => KName s t -> a -> KAbs (KName s t) a infixr 0 Source #

The abstraction pattern '(:>)' is just an instance of '(:@!)' for KAbs. Thus,

n :@> x -> f n x

is synonymous with

x' -> x' @@! f 

Because '(:>)' is a concrete instance of '(:!)', we can declare it COMPLETE@.

fuse :: (KAbs (KName s t) a1, KAbs (KName s t) a2) -> KAbs (KName s t) (a1, a2) Source #

Fuse abstractions, taking label of abstracted name from first argument. Should satisfy:

fuse (n @> x) (n @> y) = n @> (x, y)

unfuse :: KAbs (KName s t) (a, b) -> (KAbs (KName s t) a, KAbs (KName s t) b) Source #

Split two abstractions. Should satisfy:

unfuse (n @> (x,y)) = (n @> x, n @> y)

absLabel :: KAbs (KName s t) a -> t Source #

Return the label of an abstraction.

Note: For reasons having to do with the Haskell type system it's convenient to store this label in the underlying representation of the abstraction, using a "dummy name". However, we do not export access to this name, we only export access to its label, using absLabel.

conc :: BinderConc ctxbody ctx body s a => ctxbody -> a -> body Source #

The bijection between Abs and KNom

absToNom :: (Typeable s, Swappable t, Swappable a) => KAbs (KName s t) a -> KNom s (KName s t, a) Source #

Bijection between Nom and Abs. Just an instance of binderToNom.

nomToAbs :: (Typeable s, Swappable t, Swappable a) => KNom s (KName s t, a) -> KAbs (KName s t) a Source #

Bijection between Nom and Abs. Just an instance of nomToBinder.

Unpacking name-contexts and abstractions

absFresh :: (Typeable s, Swappable t, Swappable a) => t -> (KName s t -> a) -> KAbs (KName s t) a Source #

Apply f to a fresh element with label t

absFresh' :: (Typeable s, Swappable t, Swappable a, Default t) => (KName s t -> a) -> KAbs (KName s t) a Source #

Apply f to a fresh element with default label

absFuncOut :: (Typeable s, Swappable t, Swappable a, Swappable b, Default t) => (KAbs (KName s t) a -> KAbs (KName s t) b) -> KAbs (KName s t) (a -> b) Source #

Near inverse to applicative distribution. absFuncIn . absFuncOut = id but not necessarily other way around

Tests

Property-based tests are in Language.Nominal.Properties.AbsSpec.