**Module Prelude**

## Meta-data

**Description**: Common functions for Granule programs**Authors**: Dominic Orchard, Vilem-Benjamin Liepelt**License**: BSD3**Copyright**: (c) Authors 2018**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]

'Comultiplication' operation showing that graded necessity is a graded comonad

extract : forall {a : Type, s : Coeffect, r : s} . {((1 : s)) ≤ r} => a [r] -> a

'Counit' operation showing that graded necessity is a graded comonad

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)