Function.fm

// Function.fm
// ===========
// 
// Wrapper and utilities for the built-in function type.

import Equal
import Pair

// Definition
// ----------

// A dependent function
Function(A: Type, B: A -> Type) : Type
  (x: A) -> B(x)

// Operations
// ----------

// The identity function
id(A; x: A) : A
  x

// The constant function always returns the same value
const(A; B; x: A, y: B) : A
  x

// dependent composition
comp(A; B; C: B -> Type)
: (g: (b: B) -> C(b), f: A -> B, x: A) -> C(f(x))
  (g, f, x) => g(f(x))

// uncurry 2-ary function
uncurry(A; B; C; f: A -> B -> C, p: Pair(A, B)) : C
  case p
  | pair => f(p.fst, p.snd)

curry(A; B; C; f: Pair(A,B) -> C, x: A, y: B) : C
  f(pair(__ x,y))

// Flip the term arguments
flip(A; B; C; f: A -> B -> C, y: B, x: A) : C
  f(x, y)

// Applies a function to an argument
call(A; B; f: A -> B, x: A) : B
  f(x)

// Pipes an argument to a function
pipe(A; B; x: A, f: A -> B) : B
  f(x)