Built-in primitives

Meta-data

Contents

[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