Skip to content

Commit

Permalink
Add functor test.
Browse files Browse the repository at this point in the history
  • Loading branch information
skaller committed May 23, 2022
1 parent 12dc4e2 commit f89eddb
Showing 1 changed file with 36 additions and 0 deletions.
36 changes: 36 additions & 0 deletions src/test/regress/rt/functor01.fdoc
Original file line number Diff line number Diff line change
@@ -0,0 +1,36 @@
@h1 Functor composition
@felix

typefun comp<J,K,L>
(f: K->J, g :L -> K):L -> J
=> fun (t:L):J => f(g(t))
;


typedef pair = fun (A:TYPE, B:TYPE):TYPE => A * B;
typedef diag = fun (X: TYPE): TYPE * TYPE => X, X;

// we want to construct the functor equivalent to this:
typedef pairofdiag = fun (T:TYPE):TYPE=> pair(diag(T));
var x: pairofdiag int = 1,2;
println$ x;

// So here, g is diag: TYPE-> TYPE * TYPE
// and f is pair: TYPE * TYPE -> TYPE
// J is f codomain, the final result TYPE
// K is f domain, and g codomain TYPE * TYPE
// L is g domain, TYPE
// so the composite is TYPE -> TYPE

typedef pairofdiag2 = comp<TYPE,TYPE * TYPE, TYPE> (pair, diag);

var y : pairofdiag2 int = 1,2;
println$ y;

typedef pairofdiag3 = comp(pair, diag); // J,K,L deduced!
var z : pairofdiag3 int = 1,2;
println$ z;

@expect
@

0 comments on commit f89eddb

Please sign in to comment.