Std

The standard library, implicitly impoted. Entries in italics are supertypes of existing types, for convenience.

Literals & Entities

type Entity

== : Entity -> Entity -> Boolean
Entity equality.

/= : Entity -> Entity -> Boolean
Entity non-equality.

entityAnchor : Entity -> Text
The anchor of an entity, as text.

type Literal

subtype Literal <: Entity

toText : Literal -> Text
The text of a literal.

Boolean

type Boolean

subtype Boolean <: Literal

True : Boolean (also pattern)
Boolean TRUE.

False : Boolean (also pattern)
Boolean FALSE.

&& : Boolean -> Boolean -> Boolean
Boolean AND.

|| : Boolean -> Boolean -> Boolean
Boolean OR.

not : Boolean -> Boolean
Boolean NOT.

Ordering

type Ordering

LT : Ordering (also pattern)
Less than.

EQ : Ordering (also pattern)
Equal to.

GT : Ordering (also pattern)
Greater than.

eq : Ordering -> Boolean
Equal.

ne : Ordering -> Boolean
Not equal.

lt : Ordering -> Boolean
Less than.

le : Ordering -> Boolean
Less than or equal to.

gt : Ordering -> Boolean
Greater than.

ge : Ordering -> Boolean
Greater than or equal to.

alphabetical : Text -> Text -> Ordering
Alphabetical order.

numerical : Number -> Number -> Ordering
Numercal order.

chronological : Time -> Time -> Ordering
Chronological order.

durational : Duration -> Duration -> Ordering
Durational order.

calendrical : Date -> Date -> Ordering
Date order.

horological : TimeOfDay -> TimeOfDay -> Ordering
Time of day order.

localChronological : LocalTime -> LocalTime -> Ordering
Local time order.

noOrder : Any -> Any -> Ordering
No order, everything EQ.

orders : [a -> a -> Ordering] -> a -> a -> Ordering
Join orders by priority.

reverse : (a -> a -> Ordering) -> a -> a -> Ordering
Reverse an order.

Text

type Text

subtype Text <: Literal

<> : Text -> Text -> Text
Concatenate text.

textLength : Text -> Integer
The length of a piece of text.

textSection : Integer -> Integer -> Text -> Text
textSection start len text is the section of text beginning at start of length len.

textConcat : [Text] -> Text
Concatenate texts.

Numeric

~== : Number -> Number -> Boolean
Numeric equality, folding exact and inexact numbers.

~/= : Number -> Number -> Boolean
Numeric non-equality.

< : Number -> Number -> Boolean
Numeric strictly less.

<= : Number -> Number -> Boolean
Numeric less or equal.

> : Number -> Number -> Boolean
Numeric strictly greater.

>= : Number -> Number -> Boolean
Numeric greater or equal.

Integer

type Integer

subtype Integer <: Rational

parseInteger : Text -> Maybe Integer
Parse text as an integer. Inverse of toText.

interpretIntegerAsText : WholeRef Integer -> WholeRef Text
Interpret an integer reference as text, interpreting deleted values as empty text.

+ : Integer -> Integer -> Integer
Add.

- : Integer -> Integer -> Integer
Subtract.

* : Integer -> Integer -> Integer
Multiply.

negate : Integer -> Integer
Negate.

abs : Integer -> Integer
Absolute value.

signum : Integer -> Integer
Sign.

mod : Integer -> Integer -> Integer
Modulus, leftover from div

even : Integer -> Boolean
Is even?

odd : Integer -> Boolean
Is odd?

gcd : Integer -> Integer -> Integer
Greatest common divisor.

lcm : Integer -> Integer -> Integer
Least common multiple.

^ : Integer -> Integer -> Integer
Raise to non-negative power.

sum : [Integer] -> Integer
Sum.

product : [Integer] -> Integer
Product.

Rational

type Rational

subtype Rational <: Number

parseRational : Text -> Maybe Rational
Parse text as a rational. Inverse of toText.

interpretRationalAsText : WholeRef Rational -> WholeRef Text
Interpret a rational reference as text, interpreting deleted values as empty text.

.+ : Rational -> Rational -> Rational
Add.

.- : Rational -> Rational -> Rational
Subtract.

.* : Rational -> Rational -> Rational
Multiply.

/ : Rational -> Rational -> Rational
Divide.

negateR : Rational -> Rational
Negate.

recip : Rational -> Rational
Reciprocal.

absR : Rational -> Rational
Absolute value.

signumR : Rational -> Rational
Sign.

modR : Rational -> Rational -> Rational
Modulus, leftover from div

^^ : Rational -> Integer -> Rational
Raise to Integer power.

sumR : [Rational] -> Rational
Sum.

meanR : [Rational] -> Rational
Mean.

productR : [Rational] -> Rational
Product.

Number

subtype Number <: Literal

parseNumber : Text -> Maybe Number
Parse text as a number. Inverse of toText.

interpretNumberAsText : WholeRef Number -> WholeRef Text
Interpret a number reference as text, interpreting deleted values as empty text.

type Number

~+ : Number -> Number -> Number
Add.

~- : Number -> Number -> Number
Subtract.

~* : Number -> Number -> Number
Multiply.

~/ : Number -> Number -> Number
Divide.

negateN : Number -> Number
Negate.

recipN : Number -> Number
Reciprocal.

pi : Number
Half the radians in a circle.

exp : Number -> Number
Exponent

log : Number -> Number
Natural logarithm

sqrt : Number -> Number
Square root.

** : Number -> Number -> Number
Raise to power.

logBase : Number -> Number -> Number

sin : Number -> Number
Sine of an angle in radians.

cos : Number -> Number
Cosine of an angle in radians.

tan : Number -> Number
Tangent of an angle in radians.

asin : Number -> Number
Radian angle of a sine.

acos : Number -> Number
Radian angle of a cosine.

atan : Number -> Number
Radian angle of a tangent.

sinh : Number -> Number
Hyperbolic sine.

cosh : Number -> Number
Hyperbolic cosine.

tanh : Number -> Number
Hyperbolic tangent.

asinh : Number -> Number
Inverse hyperbolic sine.

acosh : Number -> Number
Inverse hyperbolic cosine.

atanh : Number -> Number
Inverse hyperbolic tangent.

nabs : Number -> Number
Absolute value.

signumN : Number -> Number
Sign. Note this will be the same exact or inexact as the number.

floor : Number -> Integer
Integer towards negative infinity.

ceiling : Number -> Integer
Integer towards positive infinity.

round : Number -> Integer
Closest Integer.

inexact : Number -> Number
Convert a number to inexact.

approximate : Rational -> Number -> Rational
approximate d x gives the exact number that's a multiple of d that's closest to x.

div : Number -> Number -> Integer
Division to Integer, towards negative infinity.

modN : Number -> Number -> Number
Modulus, leftover from div

isNaN : Number -> Boolean
Is not a number?

isInfinite : Number -> Boolean
Is infinite?

isNegativeZero : Number -> Boolean
Is negative zero?

isExact : Number -> Boolean
Is exact?

sumN : [Number] -> Number
Sum.

meanN : [Number] -> Number
Mean.

productN : [Number] -> Number
Product.

numberCheckSafeRational : Number -> Maybe Rational
Get the exact value of a Number, if it is one.

checkExactInteger : Number -> Maybe Integer
Get the exact Integer value of a Number, if it is one. Works as expected on Rationals.

Date & Time

Duration

type Duration

subtype Duration <: Literal

parseDuration : Text -> Maybe Duration
Parse text as a duration. Inverse of toText.

interpretDurationAsText : WholeRef Duration -> WholeRef Text
Interpret a duration reference as text, interpreting deleted values as empty text.

zeroDuration : Duration
No duration.

secondsToDuration : Rational -> Duration
Convert seconds to duration.

durationToSeconds : Duration -> Rational
Convert duration to seconds.

dayDuration : Duration
One day duration.

addDuration : Duration -> Duration -> Duration
Add durations.

subtractDuration : Duration -> Duration -> Duration
Subtract durations.

negateDuration : Duration -> Duration
Negate duration.

multiplyDuration : Number -> Duration -> Duration
Multiply a duration by a number.

divideDuration : Duration -> Duration -> Number
Divide durations.

Time

type Time
Absolute time as measured by UTC.

subtype Time <: Literal

parseTime : Text -> Maybe Time
Parse text as a time. Inverse of toText.

interpretTimeAsText : WholeRef Time -> WholeRef Text
Interpret a time reference as text, interpreting deleted values as empty text.

unixFormatTime : Text -> Time -> Text
Format a time as text, using a UNIX-style formatting string.

unixParseTime : Text -> Text -> Maybe Time
Parse text as a time, using a UNIX-style formatting string.

unixInterpretTimeAsText : Text -> WholeRef Time -> WholeRef Text
Interpret a time reference as text, interpreting deleted values as empty text.

addTime : Duration -> Time -> Time
Add duration to time.

diffTime : Time -> Time -> Duration
Difference of times.

getTime : Action Time
Get the current time.

newClock : Duration -> Action (WholeRef +Time)
Make a reference to the current time that updates per the given duration.

Calendar

type Date

MkDate : Integer -> Integer -> Integer -> Date (also pattern)
Construct a Date from year, month, day.

subtype Date <: Literal

parseDate : Text -> Maybe Date
Parse text as a date. Inverse of toText.

interpretDateAsText : WholeRef Date -> WholeRef Text
Interpret a date reference as text, interpreting deleted values as empty text.

unixFormatDate : Text -> Date -> Text
Format a date as text, using a UNIX-style formatting string.

unixParseDate : Text -> Text -> Maybe Date
Parse text as a date, using a UNIX-style formatting string.

unixInterpretDateAsText : Text -> WholeRef Date -> WholeRef Text
Interpret a date reference as text, interpreting deleted values as empty text.

dateToModifiedJulian : Date -> Integer
Convert to MJD.

modifiedJulianToDate : Integer -> Date
Convert from MJD.

addDays : Integer -> Date -> Date
Add count to days to date.

diffDays : Date -> Date -> Integer
Difference of days between dates.

getUTCDate : Action Date
Get the current UTC date.

getDate : Action Date
Get the current local date.

Time of Day

type TimeOfDay

MkTimeOfDay : Integer -> Integer -> Rational -> TimeOfDay (also pattern)
Construct a TimeOfDay from hour, minute, second.

subtype TimeOfDay <: Literal

parseTimeOfDay : Text -> Maybe TimeOfDay
Parse text as a time of day. Inverse of toText.

interpretTimeOfDayAsText : WholeRef TimeOfDay -> WholeRef Text
Interpret a time of day reference as text, interpreting deleted values as empty text.

unixFormatTimeOfDay : Text -> TimeOfDay -> Text
Format a time of day as text, using a UNIX-style formatting string.

unixParseTimeOfDay : Text -> Text -> Maybe TimeOfDay
Parse text as a time of day, using a UNIX-style formatting string.

unixInterpretTimeOfDayAsText : Text -> WholeRef TimeOfDay -> WholeRef Text
Interpret a time of day reference as text, interpreting deleted values as empty text.

midnight : TimeOfDay
Midnight.

midday : TimeOfDay
Midday.

Local Time

type LocalTime

MkLocalTime : Date -> TimeOfDay -> LocalTime (also pattern)
Construct a LocalTime from day and time of day.

subtype LocalTime <: Literal

parseLocalTime : Text -> Maybe LocalTime
Parse text as a local time. Inverse of toText.

interpretLocalTimeAsText : WholeRef LocalTime -> WholeRef Text
Interpret a local time reference as text, interpreting deleted values as empty text.

unixFormatLocalTime : Text -> LocalTime -> Text
Format a local time as text, using a UNIX-style formatting string.

unixParseLocalTime : Text -> Text -> Maybe LocalTime
Parse text as a local time, using a UNIX-style formatting string.

unixInterpretLocalTimeAsText : Text -> WholeRef LocalTime -> WholeRef Text
Interpret a local time reference as text, interpreting deleted values as empty text.

timeToLocal : Integer -> Time -> LocalTime
Convert a time to local time, given a time zone offset in minutes

localToTime : Integer -> LocalTime -> Time
Convert a local time to time, given a time zone offset in minutes

getTimeZone : Time -> Action Integer
Get the offset for a time in the current time zone.

getCurrentTimeZone : Action Integer
Get the current time zone offset in minutes.

getLocalTime : Action LocalTime
Get the current local time.

newTimeZoneRef : WholeRef +Time -> Action (WholeRef +Integer)
The current time zone offset in minutes.

Open Entity Types

openEntity @A <anchor> : A
An open entity for this anchor. A is an open entity type.

newOpenEntity @A : Action A
Generate an open entity. A is an open entity type.

Dynamic Entity Types

type DynamicEntity

subtype (any dynamic entity type) <: Entity

dynamicEntity @A <anchor> : A
A dynamic entity for this anchor. A is a concrete dynamic entity type.

newDynamicEntity @A : Action A
Generate a dynamic entity. A is a concrete dynamic entity type.

Maybe

type Maybe

Just : a -> Maybe a (also pattern)
Construct a Maybe from a value.

Nothing : Maybe None (also pattern)
Construct a Maybe without a value.

subtype Maybe Entity <: Entity

Pairs

subtype (Entity,Entity) <: Entity

fst : (a, b) -> a
Get the first member of a pair.

snd : (a, b) -> b
Get the second member of a pair.

toPair : a -> b -> (a, b)
Construct a pair.

pair : a -> (a, a)
Construct a pair.

Either

type Either

Left : a -> Either a b (also pattern)
Construct an Either from the left.

Right : b -> Either a b (also pattern)
Construct an Either from the right.

subtype Either Entity Entity <: Entity

fromEither : (a -> c) -> (b -> c) -> Either a b -> c
Eliminate an Either

either : Either a a -> a
Eliminate an Either

Lists

[] : [None] (also pattern)
Empty list

:: : a -> [a] -> [a] (also pattern)
Construct a list

subtype [Entity] <: Entity

list : b -> (a -> [a] -> b) -> [a] -> b
Eliminate a list

length : [Any] -> Integer
Number of items in a list

index : [a] -> Integer -> Maybe a
Get item from list by index.

mapList : (a -> b) -> [a] -> [b]
Map the items of a list.

++ : [a] -> [a] -> [a]
Concatentate lists.

filter : (a -> Boolean) -> [a] -> [a]
Filter a list.

maybeMapList : (a -> Maybe b) -> [a] -> [b]
Map and filter a list.

take : Integer -> [a] -> [a]
Take the first n elements.

drop : Integer -> [a] -> [a]
Drop the first n elements.

zip : [a] -> [b] -> [(a, b)]
Zip two lists.

Functions

id : a -> a
The identity function.

$ : (a -> b) -> a -> b
Apply a function to a value.

. : (a -> b) -> (c -> a) -> c -> b
Compose functions.

error : Text -> None
Error.

seq : Any -> a -> a
Evaluate the first argument, then if that's not "bottom" (error or non-termination), return the second argument.

check @A : D(A) -> Maybe A
Check from a dynamic supertype.

coerce @A : D(A) -> A
Coerce from a dynamic supertype.

Actions

type Action

return : a -> Action a
A value as an Action.

>>= : Action a -> (a -> Action b) -> Action b
Bind the result of an Action to an Action.

>> : Action Any -> Action a -> Action a
Do actions in sequence.

mapAction : (a -> b) -> Action a -> Action b
Map a function on an action.

fixAction : (a -> Action a) -> Action a
The fixed point of an Action.

fail : Text -> Action None
Fail, causing the program to terminate with error.

stop : Action None
Stop. This is similar to an exception that can be caught with onStop. The default handler (for the main program, button presses, etc.), is to catch and ignore it.

onStop : Action a -> Action a -> Action a
onStop p q does p first, and if it stops, then does q.

for_ : [a] -> (a -> Action ()) -> Action ()
Perform an action on each value of a list.

for : [a] -> (a -> Action b) -> Action [b]
Perform an action on each value of a list, returning a list.

output : Text -> Action ()
Output text to standard output.

outputLn : Text -> Action ()
Output text and a newline to standard output.

getTimeMS : Action Integer
Get the time as a whole number of milliseconds.

sleep : Integer -> Action ()
Do nothing for this number of milliseconds.

Lifecycle

Ways of managing the closing of things that get opened, most notably UI windows.

lifecycle : Action a -> Action a
Close everything that gets opened in the given action.

Example: lifecycle $ do openResource; sleep 1000 end
This opens some resource, sleeps for one second, and then closes it again.

onClose : Action () -> Action ()
Add this action as to be done when closing.

Example: lifecycle $ do onClose $ outputLn "hello"; sleep 1000 end
This sleeps for one second, and then outputs "hello" (when the lifecycle closes).

closer : Action a -> Action (a, Action ())
Get an (idempotent) action that closes what gets opened in the given action.

Example: (cl,r) <- closer openResource
This opens a resource r, also creating an action cl, that will close the resource when first called (subsequent calls do nothing). This action will also be run at the end of the lifecycle, only if it hasn't already.

Interpreter

evaluate @A : Text -> Action (Either Text A)
A function that evaluates text as a Pinafore expression to be subsumed to positive type A.

The result of the action is either the value (Right), or an error message (Left).

The local scope is not in any way transmitted to the evaluation.

Invocation

How the script was invoked.

scriptName : Text
The name of the script.

scriptArguments : [Text]
Arguments passed to the script.

environment : [(Text, Text)]
Environment variables.

getEnv : Text -> Maybe Text
Get environment variable.

Undo

Undo and redo changes.

queueUndo : Action Boolean
Undo an action.

queueRedo : Action Boolean
Redo an action.

References

References keep track of updates, and will update user interfaces constructed from them when their value changes.

Whole References

type WholeRef
A whole reference of type WholeRef {-p,\+q} has a setting type of p and a getting type of q.

pureWhole : a -> WholeRef +a
A constant whole reference for a value.

immutWhole : WholeRef +a -> WholeRef +a
Convert a whole reference to immutable. immutWhole r = {%r}

coMapWhole : (a -> b) -> WholeRef {-c,+a} -> WholeRef {-c,+b}
Map a function on getting a whole reference.

contraMapWhole : (b -> a) -> WholeRef {-a,+c} -> WholeRef {-b,+c}
Map a function on setting a whole reference.

maybeLensMapWhole : (Maybe aq -> Maybe bq) -> (Maybe bp -> Maybe aq -> Maybe (Maybe ap)) -> WholeRef {-ap,+aq} -> WholeRef {-bp,+bq}
Map getter & pushback functions on a whole reference.

lensMapWhole : (aq -> b) -> (b -> Maybe aq -> Maybe ap) -> WholeRef {-ap,+aq} -> WholeRef b
Map getter & pushback functions on a whole reference.

toMaybeWhole : WholeRef {-a,+b} -> WholeRef {-(Maybe a),+(Maybe b)}
Map known/unknown to Maybe for a whole reference.

fromMaybeWhole : WholeRef {-(Maybe a),+(Maybe b)} -> WholeRef {-a,+b}
Map Maybe to known/unknown for a whole reference.

forWhole : [a] -> (a -> WholeRef +b) -> WholeRef +[b]
Traverse a list to make a reference to a list.

pairWhole : WholeRef {-ap,+aq} -> WholeRef {-bp,+bq} -> WholeRef {-(ap, bp),+(aq, bq)}
Combine whole references.

applyWhole : WholeRef +(a -> b) -> WholeRef +a -> WholeRef +b
Combine getting of whole references. applyWhole f x = {%f %x}

unknown : WholeRef {}
The unknown whole reference, representing missing information.

known : WholeRef {} -> WholeRef +Boolean
True if the whole reference is known.

?? : WholeRef +a -> WholeRef +a -> WholeRef +a
p ?? q = p if it is known, else q.

get : WholeRef +a -> Action a
Get a whole reference, or stop if the whole reference is unknown.

:= : WholeRef -a -> a -> Action ()
Set a whole reference to a value. Stop if failed.

delete : WholeRef {} -> Action ()
Delete a whole reference (i.e., make unknown). Stop if failed.

subscribeWhole : WholeRef +a -> (Maybe a -> Action ()) -> Action ()
Do an action initially and on every update, until closed.

newMemWhole : Action (WholeRef a)
Create a new whole reference to memory, initially unknown.

Set References

type SetRef

mapSet : (a -> b) -> SetRef b -> SetRef a
Map a function on a set.

pureSet : (a -> Boolean) -> SetRef (Entity & a)
Convert a predicate to a set.

refSet : WholeRef {-((Entity & a) -> Boolean),+(a -> Boolean)} -> SetRef (Entity & a)
Convert a predicate reference to a set.

immutSet : SetRef a -> SetRef a
Convert a set to immutable.

+= : SetRef a -> a -> Action ()
Add an entity to a set.

-= : SetRef a -> a -> Action ()
Remove an entity from a set.

member : SetRef a -> WholeRef +a -> WholeRef Boolean
A reference to the membership of a value in a set.

notSet : SetRef a -> SetRef a
Complement of a set. The resulting set can be added to (deleting from the original set) and deleted from (adding to the original set).

<&> : SetRef a -> SetRef a -> SetRef a
Intersection of sets. The resulting set can be added to (adding to both sets), but not deleted from.

<|> : SetRef a -> SetRef a -> SetRef a
Union of sets. The resulting set can be deleted from (deleting from both sets), but not added to.

<\> : SetRef a -> SetRef a -> SetRef a
Difference of sets, everything in the first set but not the second. The resulting set can be added to (adding to the first and deleting from the second), but not deleted from.

<^> : SetRef a -> SetRef a -> SetRef a
Symmetric difference of sets, everything in exactly one of the sets. The resulting set will be read-only.

<+> : SetRef a -> SetRef b -> SetRef (Either a b)
Cartesian sum of sets.

<*> : SetRef a -> SetRef b -> SetRef (a, b)
Cartesian product of sets. The resulting set will be read-only.

Finite Set References

type FiniteSetRef

subtype FiniteSetRef -a <: SetRef a

coMapFiniteSet : (a -> b) -> FiniteSetRef {-c,+a} -> FiniteSetRef {-c,+b}
Map a function on getting from a finite set.

contraMapFiniteSet : (b -> a) -> FiniteSetRef {-a,+c} -> FiniteSetRef {-b,+c}
Map a function on setting to and testing a finite set.

maybeMapFiniteSet : (aq -> Maybe b) -> FiniteSetRef {-ap,+aq} -> FiniteSetRef {b,-ap}
Map and filter a function on a finite set.

<:&> : FiniteSetRef {-a,+b} -> SetRef b -> FiniteSetRef {-a,+b}
Intersect a finite set with any set. The resulting finite set will be read-only.

<:\> : FiniteSetRef {-a,+b} -> SetRef b -> FiniteSetRef {-a,+b}
Difference of a finite set and any set. The resulting finite set will be read-only.

<:&:> : FiniteSetRef {a,+Entity} -> FiniteSetRef {a,+Entity} -> FiniteSetRef {a,-Entity}
Intersection of finite sets. The resulting finite set can be added to, but not deleted from.

<:|:> : FiniteSetRef {a,+Entity} -> FiniteSetRef {a,+Entity} -> FiniteSetRef {a,-Entity}
Union of finite sets. The resulting finite set can be deleted from, but not added to.

<:+:> : FiniteSetRef {-ap,+aq} -> FiniteSetRef {-bp,+bq} -> FiniteSetRef {-(Either ap bp),+(Either aq bq)}
Cartesian sum of finite sets.

<:+:> : FiniteSetRef a -> FiniteSetRef b -> FiniteSetRef (Either a b)
Cartesian sum of finite sets.

<:*:> : FiniteSetRef {-ap,+aq} -> FiniteSetRef {-bp,+bq} -> FiniteSetRef {-(ap, bp),+(aq, bq)}
Cartesian product of finite sets. The resulting finite set will be read-only.

<:*:> : FiniteSetRef a -> FiniteSetRef b -> FiniteSetRef (a, b)
Cartesian product of finite sets. The resulting finite set will be read-only.

setList : RefOrder a -> FiniteSetRef +a -> WholeRef +[a]
All members of a finite set, by an order.

getSetList : RefOrder a -> FiniteSetRef {a,+Entity} -> Action (ListRef +a)
Get all members of a finite set, by an order. The resulting ListRef will behave more "list-like" than setList.

listSet : WholeRef {-[a],+[Entity & a]} -> FiniteSetRef {a,-Entity}
Represent a reference to a list as a finite set. Changing the set may scramble the order of the list.

setSingle : FiniteSetRef {+Entity,+a} -> WholeRef +a
The member of a single-member finite set, or unknown.

setCount : FiniteSetRef {} -> WholeRef +Integer
Count of members in a finite set.

setClear : FiniteSetRef {} -> Action ()
Remove all entities from a finite set.

newMemFiniteSet : Action (FiniteSetRef {a,-Entity})
Create a new finite set reference to memory, initially empty.

List References

type ListRef

subtype WholeRef [a] <: ListRef a

listWhole : ListRef a -> WholeRef [a]
Represent a list reference as a whole reference.

listGetCount : ListRef {} -> Action Integer
Get Count of elements in a list reference.

listGetItem : Integer -> ListRef +q -> Action q
Get an element of a list reference.

listInsert : Integer -> p -> ListRef -p -> Action ()
Insert an element in a list reference.

listSet : Integer -> p -> ListRef -p -> Action ()
Set an element of a list reference.

listDelete : Integer -> ListRef {} -> Action ()
Delete an element of a list reference.

listClear : ListRef {} -> Action ()
Delete all elements of a list reference.

listCountRef : ListRef {} -> WholeRef +Integer
Reference to a count of elements in a list reference.

listGetItemRef : Boolean -> Integer -> ListRef {-p,+q} -> Action (WholeRef {-p,+q})
Get a whole reference to a particular item in the list. It will track the item as the list changes. Pass True for an existing item, False for a point between items.

newMemList : Action (ListRef a)
Create a new list reference to memory, initially empty.

Morphisms

Morphisms relate entities.

identity : {-x,+y} ~> {-y,+x}
The identity morphism.

!. : ({-bx,+by} ~> {-cp,+cq}) -> ({-ap,+aq} ~> {-by,+bx}) -> {-ap,+aq} ~> {-cp,+cq}
Compose morphisms.

!. : (b ~> c) -> (a ~> b) -> a ~> c
Compose morphisms.

!** : ({-ap,+Entity,+aq} ~> {-bp,+bq}) -> ({-ap,+Entity,+aq} ~> {-cp,+cq}) -> {-ap,+aq} ~> {-(bp, cp),+(bq, cq)}
Pair morphisms. References from these morphisms are undeleteable.

!** : ({a,+Entity} ~> b) -> ({a,+Entity} ~> c) -> a ~> (b, c)
Pair morphisms. References from these morphisms are undeleteable.

!++ : ({-ap,+aq} ~> {-cp,+cq}) -> ({-bp,+bq} ~> {-cp,+cq}) -> {-(Either ap bp),+(Either aq bq)} ~> {-cp,+cq}
Either morphisms. References from these morphisms are undeleteable.

!++ : (a ~> c) -> (b ~> c) -> (Either a b) ~> c
Either morphisms. References from these morphisms are undeleteable.

!$ : ({-ap,+aq} ~> {-bp,+bq}) -> WholeRef {-aq,+ap} -> WholeRef {-bp,+bq}
Apply a morphism to a reference.

!$ : (a ~> b) -> WholeRef a -> WholeRef b
Apply a morphism to a reference.

!$% : (-a ~> {-bp,+bq}) -> WholeRef +a -> WholeRef {-bp,+bq}
Apply a morphism to an immutable reference. m !$% r = m !$ immutWhole r

!$% : (-a ~> b) -> WholeRef +a -> WholeRef b
Apply a morphism to an immutable reference. m !$% r = m !$ immutWhole r

!$$ : (-a ~> {+Entity,+b}) -> FiniteSetRef +a -> FiniteSetRef {b,-Entity}
Apply a morphism to a set.

!@ : ({a,+Entity} ~> {-bx,+by}) -> WholeRef {-by,+bx} -> FiniteSetRef {a,-Entity}
Co-apply a morphism to a reference.

!@ : ({a,+Entity} ~> b) -> WholeRef b -> FiniteSetRef {a,-Entity}
Co-apply a morphism to a reference.

!@% : ({a,+Entity} ~> -b) -> WholeRef +b -> FiniteSetRef {a,-Entity}
Co-apply a morphism to an immutable reference. m !@% r = m !@ immutWhole r

!@@ : ({a,+Entity} ~> {-bx,+by}) -> FiniteSetRef {-by,+bx} -> FiniteSetRef {a,-Entity}
Co-apply a morphism to a set.

!@@ : ({a,+Entity} ~> b) -> FiniteSetRef b -> FiniteSetRef {a,-Entity}
Co-apply a morphism to a set.

property @A @B <anchor> : A ~> B
A property for this anchor. A and B are types that are subtypes of Entity.

RefOrders

type RefOrder

subtype a -> a -> Ordering <: RefOrder a

orders : [RefOrder a] -> RefOrder a
Join RefOrders by priority.

mapOrder : (b -> a) -> RefOrder a -> RefOrder b
Map a function on a RefOrder.

orderOn : (-b ~> +a) -> RefOrder a -> RefOrder b
Order by a RefOrder on a particular morphism.

reverseOrder : RefOrder a -> RefOrder a
Reverse a RefOrder.

orderWhole : RefOrder a -> WholeRef +a -> WholeRef +a -> WholeRef +Ordering
Order two whole references.

Files

NYI