Module Prelude

## Meta-data

• Description: Common functions for Granule programs
• Authors: Dominic Orchard, Vilem-Benjamin Liepelt
• Issue-tracking: https://github.com/dorchard/granule/issues
• Repository: https://github.com/dorchard/granule

## Contents

### [top] Standard functional components

```id : forall {a : Type}
. a -> a```
Identity function
```flip : forall {a : Type, b : Type, c : Type}
. (a -> b -> c) -> b -> a -> c```
Flip the order of parameters
```const : forall {a : Type, b : Type, s : Coeffect}
. a -> (b [(0 : s)]) -> a```
Constant combinator NB: Throws away its second argument and returns the first
```lcompose : forall {a : Type, b : Type, c : Type}
. (b -> c) -> (a -> b) -> a -> c```
linear function composition (the composition operator g ∘ f resolves to whatever is bound to compose)
```until : forall {a : Type}
. ((a -> Bool) [1..∞]) -> ((a -> a) [0..∞]) -> (a [2..∞]) -> a```
Apply f to x until p holds
```if0 : forall {a : Type}
. (Int [0..1]) -> (a [0..1]) -> (a [0..1]) -> a```
Conditional on integers Returns x if g is zero, else returns y

### [top] Numeric functions and constants

`sign : (Int [1..2]) -> Int`
Given some n, return + 1 iff n is positive + -1 iff n is negative + 0 otherwise
`pi : Float`
An approximation of pi
`e : Float`
An approximation of Euler's number

### [top] Combinators involving products (pairs)

```fst : forall {a : Type, b : Type, s : Coeffect}
. (a, b [(0 : s)]) -> a```
Extract the left part of a pair
```snd : forall {a : Type, b : Type, s : Coeffect}
. (a [(0 : s)], b) -> b```
Extract the right part of a pair
```curry : forall {a : Type, b : Type, c : Type}
. ((a, b) -> c) -> a -> b -> c```
curry converts an uncurried function to a curried function
```uncurry : forall {a : Type, b : Type, c : Type}
. (a -> b -> c) -> (a, b) -> c```
uncurry converts a curried function to a function on pairs

### [top] Semiring-polymorphic combinators

```comp : forall {k : Coeffect, n : k, m : k, a : Type, b : Type, c : Type}
. ((b [n]) -> c) -> (((a [m]) -> b) [n]) -> (a [n * m]) -> c```
Coeffectful composition
```boxmap : forall {a : Type, b : Type, s : Coeffect, r : s}
. ((a -> b) [r]) -> (a [r]) -> b [r]```
Graded necessity is an applicative functor
```disject : forall {a : Type, k : Coeffect, n : k, m : k}
. (a [m * n]) -> (a [n]) [m]```
```extract : forall {a : Type, s : Coeffect, r : s}
. {((1 : s)) ≤ r} =>
(a [r]) -> a```
```pushPair : forall {a : Type, b : Type, k : Coeffect, c : k}
. {Pushable c} =>
((a, b) [c]) -> (a [c], b [c])```
Push coeffects on a pair into the left and right elements. A distributive law of graded necessity over products. Note however that this is not always defined: the operation {c ⨱ c} is partial and is only defined if the semiring k permits this behaviour at c. (An example of a semiring where this is not true is for k = LNL and c = 1).
```pullPair : forall {a : Type, b : Type, k : Coeffect, n : k}
. (a [n], b [n]) -> (a, b) [n]```
Pull coeffects of pair elements outside of the pair
```copy : forall {a : Type, s : Coeffect}
. (a [(1 + 1 : s)]) -> (a, a)```
Generic copying of a value into a pair

### [top] Coeffect-specifc combinators

```flatten : forall {a : Type, n : Nat, m : Nat}
. ((a [n]) [m]) -> a [n * m]```
Flatten two boxes (with Nat grading)
```unflatten : forall {a : Type, n : Nat, m : Nat}
. (a [n * m]) -> (a [n]) [m]```
Expand two boxes (with Nat grading)