Granule documentation

Built-in primitives

Meta-data

Description: Built-in primitive definitions

[top]Built-in Types

data Type : Type 1 where
    Coeffect       : Type
  ; Effect         : Type
  ; Guarantee      : Type
  ; Permission     : Type
  ; Predicate      : Type
  ; ->             : Type -> Type -> Type
  ; Int            : Type
  ; Float          : Type
  ; DFloat         : Type
  ; Char           : Type
  ; Void           : Type
  ; String         : Type
  ; Inverse        : Type -> Type
  ; Protocol       : Type
  ; Rename         : Name -> Type -> Type
  ; Chan           : Protocol -> Type
  ; LChan          : Protocol -> Type
  ; Name           : Type -> Type
  ; FloatArray     : Name -> Type
  ; Ref            : Name -> Type -> Type
  ; CapabilityType : Capability -> Type

data Coeffect : Type 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 where
    Com        : Effect
  ; IO         : Effect
  ; Exception  : Effect
  ; GradedFree : (eff : Effect) -> (eff -> Type -> Type) -> Effect

data Guarantee : Type where
    Uniqueness : Guarantee
  ; Integrity  : Guarantee

data Permission : Type where
    Fraction : Permission

data Predicate : Type where
    Dropable       : Type -> Predicate
  ; Cloneable      : Type -> Predicate
  ; ExactSemiring  : Semiring -> Predicate
  ; Mutable        : Fraction -> Predicate
  ; NonInterfering : Coeffect -> 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 Fraction : Permission where
    Star : Fraction

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] Algebraic effects and handlers

call : forall {eff : Effect, s : Coeffect, grd : s, i : Type, o : Type, r : Type, sig : eff -> Type -> Type, e : eff} 
     . (i -> ((o -> r) [grd]) -> sig e r) -> i -> o <Eff eff sig e>

Lift a CPS-style effect operation to direct-style, also called the "generic effect" operation

handle : forall {eff : Effect, sig : eff -> Type -> Type, a : Type, b : Type, e : eff} 
       . (fmap : (forall {a : Type} . forall {b : Type} . forall {l : eff} . ((a -> b) [0..∞]) -> (sig l a) -> sig l b) [0..∞]) -> ((forall {l : eff} . (sig l b) -> b) [0..∞]) -> (a -> b) -> (a <Eff eff sig e>) -> b

Deploy an effect handler on a computation tree

handleGr : forall {eff : Effect, sig : eff -> Type -> Type, a : Type, b : eff -> Type, e : eff} 
         . (fmap : (forall {a : Type} . forall {b : Type} . forall {l : eff} . ((a -> b) [0..∞]) -> (sig l a) -> sig l b) [0..∞]) -> (forall {l : eff} . (forall {j : eff} . (sig l (b j)) -> b (l * j)) [0..∞]) -> (a -> b ((1 : eff))) -> (a <Eff eff sig e>) -> b e

Deploy an effect handler on a computation tree for a graded algebra

[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, s : Coeffect, r : s} 
             . (*a) -> a [r]

reveal : forall {a : Type} 
       . (a *Trusted) -> a [Lo]

trustedBind : forall {a : Type, b : Type} 
            . ((a *Trusted) -> b [Lo]) -> (a [Lo]) -> b [Lo]

withBorrow : forall {a : Type, b : Type} 
           . ((& 1 a) -> & 1 b) -> (*a) -> *b

split : forall {a : Type, f : Fraction} 
      . {f ≠ Star} =>
    (& f a) -> (& (f * 1/2) a, & (f * 1/2) a)

join : forall {a : Type, f : Fraction, g : Fraction} 
     . {f ≠ Star, g ≠ Star} =>
    (& f a, & g a) -> & (f + g) a

borrowPush : forall {a : Type, b : Type, p : Permission, f : p} 
           . (& f (a, b)) -> (& f a, & f b)

borrowPull : forall {a : Type, b : Type, p : Permission, f : p} 
           . (& f a, & f b) -> & f (a, b)

[top] Mutable array operations

newFloatArray : Int -> exists {id : Name} 
              . *(FloatArray id)

readFloatArray : forall {p : Permission, f : p, id : Name} 
               . (& f (FloatArray id)) -> Int -> (Float, & f (FloatArray id))

writeFloatArray : forall {id : Name, f : Fraction} 
                . {mut f} =>
    (& f (FloatArray id)) -> Int -> Float -> & f (FloatArray id)

lengthFloatArray : forall {p : Permission, f : p, id : Name} 
                 . (& f (FloatArray id)) -> (!Int, & f (FloatArray id))

deleteFloatArray : forall {id : Name} 
                 . (*(FloatArray id)) -> ()

[top] Mutable reference cells

newRef : forall {a : Type} 
       . a -> exists {id : Name} . *(Ref id a)

swapRef : forall {a : Type, f : Fraction, id : Name} 
        . {mut f} =>
    (& f (Ref id a)) -> a -> (a, & f (Ref id a))

freezeRef : forall {a : Type, id : Name} 
          . (*(Ref id a)) -> a

readRef : forall {a : Type, s : Coeffect, q : s, r : s, p : Permission, f : p, id : Name} 
        . (& f (Ref id (a [q + r]))) -> (a [q], & f (Ref id (a [r])))

[top] Immutable array operations

newFloatArrayI : forall {id : Name} 
               . Int -> FloatArray id

readFloatArrayI : forall {id : Name} 
                . (FloatArray id) -> Int -> (Float, FloatArray id)

writeFloatArrayI : forall {id : Name} 
                 . (FloatArray id) -> Int -> Float -> FloatArray id

lengthFloatArrayI : forall {id : Name} 
                  . (FloatArray id) -> (Int, FloatArray id)

[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

drop : forall {a : Type} 
     . {Dropable a} =>
    a -> ()

copyShape : forall {a : Type, f : Type -> Type} 
          . (f a) -> (f (), f a)