Granule documentation

Built-in primitives

Meta-data

Description: Built-in primitive definitions

[top]Built-in Types

data Type : Type 1 where
    ->             : Type -> Type -> Type
  ; Int            : Type
  ; Float          : Type
  ; DFloat         : Type
  ; Char           : Type
  ; Void           : 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
  ; GradedFree : (eff : Effect) -> (eff -> Type -> Type) -> 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] 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} 
             . (*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

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

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