#line 360 "/home/travis/build/felix-lang/felix/src/packages/core_type_constructors.fdoc"

Categorical Operators
open class Functional
{
// note: in Felix, products are uniquely decomposable, but arrows
// are not. So we cannot overload based on arrow factorisation.
// for example, the curry functions can be overloaded but
// the uncurry functions cannot be

// Note: Felix is not powerful enough to generalise these
// operation in user code, i.e. polyadic programming

change star into arrow (2 components)
fun curry[u,v,r] (f:u*v->r) : u -> v -> r => fun (x:u) (y:v) => f (x,y);

change star into arrow (3 components)
fun curry[u,v,w,r] (f:u*v*w->r) : u -> v -> w -> r => fun (x:u) (y:v) (z:w) => f (x,y,z);

change arrow into star (arity 2)
fun uncurry2[u,v,r] (f:u->v->r) : u * v -> r => fun (x:u,y:v) => f x y;

change arrow into star (arity 3)
fun uncurry3[u,v,w,r] (f:u->v->w->r) : u * v * w -> r => fun (x:u,y:v,z:w) => f x y z;

argument order permutation (2 components)
fun twist[u,v,r] (f:u*v->r) : v * u -> r => fun (x:v,y:u) => f (y,x);

projection 1 (2 components)
fun proj1[u1,u2,r1,r2] (f:u1*u2->r1*r2) : u1 * u2 -> r1 =>
fun (x:u1*u2) => match f x with | a,_ => a endmatch;

projection 2 (2 components)
fun proj2[u1,u2,r1,r2] (f:u1*u2->r1*r2) : u1 * u2 -> r2 =>
fun (x:u1*u2) => match f x with | _,b => b endmatch;

// aka \delta or diagonal function
fun dup[T] (x:T) => x,x;

unique product (of above projections)
// if f: C-> A and g: C -> B there is a unique function
// <f,g>: C -> A * B such that f = <f,g> \odot \pi0 and
// g = <f,g> \odot pi1
// WHAT IS THE FUNCTION CALLED?

fun prdx[u1,r1,r2] (f1:u1->r1,f2:u1->r2) : u1 -> r1 * r2 =>
fun (x1:u1) => f1 x1, f2 x1;

series composition (2 functions)
fun compose[u,v,w] (f:v->w, g:u->v) : u -> w =>
fun (x:u) => f (g x)
;

fun $$\circ$$ [u,v,w] (f:v->w, g:u->v) : u -> w =>
fun (x:u) => f (g x)
;

series reverse composition (2 functions)
fun rev_compose[u,v,w] (f:u->v, g:v->w) : u -> w =>
fun (x:u) => g (f x)
;

series reverse composition (2 functions)
fun $$\odot$$[u,v,w] (f:u->v, g:v->w) : u -> w =>
fun (x:u) => g (f x)
;

}