
Meta-data
- Description: Built-in primitive definitions
Contents
- Built-in Types
- Core linear functional combinators
- Arithmetic
- Graded Possiblity
- I/O
- Exceptions
- Conversions
- Concurrency and Session Types
- Non-linear communication and concurrency patterns
- Concurrency primitives using side effects
- File Handles
- Char
- String manipulation
- Cost
- Uniqueness modality
- Mutable array operations
- Imuutable array operations
- Benchmarking
- Sensitivity
[top]Built-in Types
data Type : Type 1 where -> : Type -> Type -> Type ; Int : Type ; Float : Type ; DFloat : Type ; Char : Type ; String : Type ; Inverse : Type -> Type ; Protocol : Type ; Chan : Protocol -> Type ; LChan : Protocol -> Type ; FloatArray : Type ; CapabilityType : Capability -> Type
data Coeffect : Type 2 where ,, : Coeffect -> Coeffect -> Coeffect ; Nat : Coeffect ; Q : Coeffect ; OOZ : Coeffect ; LNL : Coeffect ; Set : Type -> Coeffect ; SetOp : Type -> Coeffect ; Cartesian : Coeffect ; Sec : Coeffect ; Interval : Coeffect -> Coeffect ; Ext : Coeffect -> Coeffect
data Effect : Type 2 where Com : Effect ; IO : Effect ; Exception : Effect
data Guarantee : Type 2 where Uniqueness : Guarantee ; Integrity : Guarantee
data Predicate : Type 2 where Dropable : Type -> Predicate ; ExactSemiring : Semiring -> Predicate ; SingleAction : Protocol -> Predicate ; ReceivePrefix : Protocol -> Predicate ; Sends : Nat -> Protocol -> Predicate
data Protocol : Type where Graded : Nat -> Protocol -> Protocol ; Send : Type -> Protocol -> Protocol ; Recv : Type -> Protocol -> Protocol ; End : Protocol ; Select : Protocol -> Protocol -> Protocol ; Offer : Protocol -> Protocol -> Protocol ; Dual : Protocol -> Protocol
data LNL : Coeffect where Zero : LNL ; One : LNL ; Many : LNL
data Cartesian : Coeffect where Any : Cartesian
data Sec : Coeffect where Hi : Sec ; Lo : Sec
data Uniqueness : Guarantee where Unique : Uniqueness
data Integrity : Guarantee where Trusted : Integrity
data Exception : Effect where Success : Exception ; MayFail : Exception
[top] Core linear functional combinators
data () where ()
Unit type
use : forall {a : Type} . a -> a [1]
Allows a linear variable to be promoted to a graded modality specifying an exact usage of 1
compose : forall {a : Type, b : Type, c : Type} . (b -> c) -> (a -> b) -> a -> c
Linear function composition
[top] Arithmetic
div : Int -> Int -> Int
Integer division
[top] Graded Possiblity
pure : forall {a : Type} . a -> a <Pure>
Inject into a computation for any graded monad
fromPure : forall {a : Type} . a <Pure> -> a
Extract form a pure computation
[top] I/O
data IOElem where Stdout ; Stdin ; Stderr ; Open ; Read ; Write ; IOExcept ; Close
IO effect operation information
fromStdin : String <{Stdin}>
Read from standard input
toStdout : String -> () <{Stdout}>
Write to standard output
toStderr : String -> () <{Stderr}>
Write to standard output
[top] Exceptions
throw : forall {a : Type, k : Coeffect} . (a [(0 : k)]) <MayFail>
[top] Conversions
showChar : Char -> String
intToFloat : Int -> Float
showInt : Int -> String
showFloat : Float -> String
readInt : String -> Int
[top] Concurrency and Session Types
forkLinear : forall {s : Protocol} . (LChan s -> ()) -> LChan (Dual s)
send : forall {a : Type, s : Protocol} . LChan (Send a s) -> a -> LChan s
recv : forall {a : Type, s : Protocol} . LChan (Recv a s) -> (a, LChan s)
close : LChan End -> ()
selectLeft : forall {p1 : Protocol, p2 : Protocol} . LChan (Select p1 p2) -> LChan p1
selectRight : forall {p1 : Protocol, p2 : Protocol} . LChan (Select p1 p2) -> LChan p2
offer : forall {p1 : Protocol, p2 : Protocol, a : Type} . (LChan p1 -> a) -> (LChan p2 -> a) -> LChan (Offer p1 p2) -> a
[top] Non-linear communication and concurrency patterns
forkNonLinear : forall {p : Protocol, s : Coeffect, r : s} . {SingleAction p, ExactSemiring s} => ((LChan p) [r] -> ()) -> (LChan (Dual p)) [r]
forkMulticast : forall {p : Protocol, n : Nat} . {Sends p} => (LChan (Graded n p) -> ()) -> N n -> Vec n (LChan (Dual p))
forkReplicate : forall {p : Protocol, n : Nat} . {ReceivePrefix p} => (LChan p -> ()) [0..n] -> N n -> Vec n ((LChan (Dual p)) [0..1])
forkReplicateExactly : forall {p : Protocol, n : Nat} . {ReceivePrefix p} => (LChan p -> ()) [n] -> N n -> Vec n (LChan (Dual p))
[top] Concurrency primitives using side effects
fork : forall {s : Protocol, k : Coeffect, c : k} . {SingleAction s, ExactSemiring k} => ((Chan s) [c] -> () <Session>) -> ((Chan (Dual s)) [c]) <Session>
gsend : forall {a : Type, s : Protocol} . Chan (Send a s) -> a -> (Chan s) <Session>
grecv : forall {a : Type, s : Protocol} . Chan (Recv a s) -> (a, Chan s) <Session>
gclose : Chan End -> () <Session>
[top] File Handles
data Handle : HandleType -> Type where
data HandleType where R ; W ; A ; RW
data IOMode : HandleType -> Type where ReadMode : IOMode R ; WriteMode : IOMode W ; AppendMode : IOMode A ; ReadWriteMode : IOMode RW
openHandle : forall {m : HandleType} . IOMode m -> String -> (Handle m) <{Open, IOExcept}>
readChar : Handle R -> (Handle R, Char) <{Read, IOExcept}>
readChar' : Handle RW -> (Handle RW, Char) <{Read, IOExcept}>
appendChar : Handle A -> Char -> (Handle A) <{Write, IOExcept}>
writeChar : Handle W -> Char -> (Handle W) <{Write, IOExcept}>
writeChar' : Handle RW -> Char -> (Handle RW) <{Write, IOExcept}>
closeHandle : forall {m : HandleType} . Handle m -> () <{Close, IOExcept}>
isEOF : Handle R -> (Handle R, Bool) <{Read, IOExcept}>
isEOF' : Handle RW -> (Handle RW, Bool) <{Read, IOExcept}>
[top] Char
charToInt : Char -> Int
charFromInt : Int -> Char
moveChar : Char -> Char [(0 : Ext Nat)..∞]
moveInt : Int -> Int [(0 : Ext Nat)..∞]
moveString : String -> String [(0 : Ext Nat)..∞]
[top] String manipulation
stringAppend : String -> String -> String
stringUncons : String -> Maybe (Char, String)
stringCons : Char -> String -> String
stringUnsnoc : String -> Maybe (String, Char)
stringSnoc : String -> Char -> String
[top] Cost
tick : () <1>
[top] Uniqueness modality
uniqueReturn : forall {a : Type} . *a -> !a
uniqueBind : forall {a : Type, b : Type} . (*a -> !b) -> !a -> !b
uniquePush : forall {a : Type, b : Type} . *(a, b) -> (*a, *b)
uniquePull : forall {a : Type, b : Type} . (*a, *b) -> *(a, b)
reveal : forall {a : Type} . a *Trusted -> a [Lo]
trustedBind : forall {a : Type, b : Type} . (a *Trusted -> b [Lo]) -> a [Lo] -> b [Lo]
[top] Mutable array operations
newFloatArray : Int -> *FloatArray
readFloatArray : *FloatArray -> Int -> (Float, *FloatArray)
writeFloatArray : *FloatArray -> Int -> Float -> *FloatArray
lengthFloatArray : *FloatArray -> (Int, *FloatArray)
deleteFloatArray : *FloatArray -> ()
[top] Imuutable array operations
newFloatArrayI : Int -> FloatArray
readFloatArrayI : FloatArray -> Int -> (Float, FloatArray)
writeFloatArrayI : FloatArray -> Int -> Float -> FloatArray
lengthFloatArrayI : FloatArray -> (Int, FloatArray)
[top] Benchmarking
data BenchList where BenchGroup String BenchList BenchList ; Bench Int String (Int [(0 : Ext Nat)..∞] -> () <{Stdout}>) BenchList ; Done
mkIOBenchMain : BenchList -> () <Pure>
[top] Sensitivity
scale : (k : Float) -> DFloat [k] -> DFloat
data Capability where Console ; TimeDate
cap : (c : Capability) -> () [{c}] -> CapabilityType c