Package: src/packages/core_type_constructors.fdoc
Core Type Constructors¶
key | file |
---|---|
option.flx | share/lib/std/datatype/option.flx |
unitsum.flx | share/lib/std/datatype/unitsum.flx |
tuple.flx | share/lib/std/datatype/tuple.flx |
slice.flx | share/lib/std/datatype/slice.flx |
typing.flx | share/lib/std/datatype/typing.flx |
special.flx | share/lib/std/datatype/special.flx |
functional.flx | share/lib/std/datatype/functional.flx |
Core Type Classes¶
//[special.flx]
// Core types and type classes
typedef any = any;
Type Functors¶
//[typing.flx]
open class Typing
{
typedef fun dom(t:TYPE):TYPE =>
typematch t with
| ?a -> _ => a
endmatch
;
typedef fun cod(t:TYPE):TYPE =>
typematch t with
| _ -> ?b => b
endmatch
;
typedef fun prj1(t:TYPE):TYPE =>
typematch t with
| ?a * _ => a
endmatch
;
typedef fun prj2(t:TYPE):TYPE =>
typematch t with
| _ * ?b => b
endmatch
;
/*
// THESE SHOULD PROBABLY BE FIXED OR DELETED
typedef fun type_lnot(x:TYPE):TYPE=>
typematch x with
| 0 => 1
| _ => 0
endmatch
;
typedef fun type_land(x:TYPE, y:TYPE):TYPE =>
typematch (x, y) with
| 0, _ => 0
| _,0 => 0
| _,_ => 1
endmatch
;
typedef fun type_lor(x:TYPE, y:TYPE):TYPE=>
typematch (x, y) with
| 0, 0 => 0
| _,_ => 1
endmatch
;
typedef fun type_eq(x:TYPE, y:TYPE):TYPE=>
typematch x with
| y => typematch y with | x => 1 | _ => 0 endmatch
| _ => 0
endmatch
;
typedef fun type_ne (x:TYPE, y:TYPE):TYPE=> type_lnot (type_eq (x , y));
typedef fun type_le (x:TYPE, y:TYPE):TYPE=>
typematch x with
| y => 1
| _ => 0
endmatch
;
typedef fun type_ge (x:TYPE, y:TYPE):TYPE=>
typematch y with
| x => 1
| _ => 0
endmatch
;
typedef fun type_gt (x:TYPE, y:TYPE):TYPE=> type_le (y, x);
typedef fun type_lt (x:TYPE, y:TYPE):TYPE=> type_ge (y, x);
*/
// Polymorphic type comparisons, including subtyping AND subsumption
typedef fun is_subtype (arg:TYPE, param:TYPE):BOOL =>
subtypematch arg with
| param => TRUE
| _ => FALSE
endmatch
;
typedef fun is_supertype (param:TYPE, arg:TYPE):BOOL =>
subtypematch arg with
| param => TRUE
| _ => FALSE
endmatch
;
typedef fun type_eq(a:TYPE, b:TYPE):BOOL =>
typematch a with
| b => TRUE
| _ => FALSE
endmatch
;
const memcount[t] : size = "#memcount";
const arrayindexcount[t] : size = "#arrayindexcount";
}
Option¶
//[option.flx]
// Note: some felix internals expect this to be defined here, not in a class, and
// in this order. Don't mess with it!
publish "option type"
variant opt[T] =
| None
| Some of T
;
open class Option {
instance[T with Show[T]] Str[opt[T]] {
fun str (x:opt[T]) =>
match x with
| Some x => "Some " + (str x)
| #None => "None"
endmatch
;
}
instance[T with Eq[T]] Eq[opt[T]] {
fun == : opt[T] * opt[T] -> bool =
| None, None => true
| Some x, Some y => x == y
| _ => false
;
}
inherit[T] Eq[T];
// Return the value of the option if it has any, otherwise
// returns the default value provided
fun or_else[T] (x:opt[T]) (d:T) : T =>
match x with
| Some v => v
| #None => d
endmatch
;
// Returns the first option if it has the value, otherwise
// the second option
fun or_else[T] (x:opt[T]) (alt:opt[T]) : opt[T] =>
match x with
| Some _ => x
| #None => alt
endmatch
;
// If the option has a value, call the given procedure on it
proc iter[T] (_f:T->void) (x:opt[T]) =>
match x with
| #None => {}
| Some v => { _f v; }
endmatch
;
// Convert an option to a list with either zero or one elements
ctor[T] list[T] (x:opt[T]) =>
match x with
| #None => list[T]()
| Some v => list[T](v)
endmatch
;
// True if this option has no value
pure fun is_empty[T] : opt[T] -> 2 =
| #None => true
| _ => false
;
// True if this option has a value
pure fun is_defined[T] : opt[T] -> 2 =
| #None => false
| _ => true
;
// Get the optional value; aborts if no value is available
fun get[T] : opt[T] -> T =
| Some v => v
;
// If the option has a value, apply the function to it and return a new Some value.
// If the option has no value, returns None
fun map[T,U] (_f:T->U) (x:opt[T]): opt[U] =>
match x with
| #None => None[U]
| Some v => Some(_f v)
endmatch
;
// Mimics the filter operation on a list.
// If there is a value and the predicate returns false for that value, return
// None. Otherwise return the same option object.
fun filter[T] (P:T -> bool) (x:opt[T]) : opt[T] =>
match x with
| Some v => if P(v) then x else None[T] endif
| #None => x
endmatch
;
// Make option types iterable. Iteration will loop once
// if there is a value. It's a handy shortcut for using
// the value if you don't care about the None case.
gen iterator[T] (var x:opt[T]) () = {
yield x;
return None[T];
}
}
class DefaultValue[T] {
virtual fun default[T]: 1->T;
fun or_default[T] (x:opt[T]) () =>
x.or_else #default[T]
;
}
Slice¶
//[slice.flx]
open class Slice {
variant slice[T] =
| Slice_all
| Slice_from of T
| Slice_from_counted of T * int /* second arg is count */
| Slice_to_incl of T
| Slice_to_excl of T
| Slice_range_incl of T * T
| Slice_range_excl of T * T
| Slice_one of T
| Slice_none
;
fun min[T with BoundRandomSequence[T]] (x:slice[T]) => match x with
| ( Slice_all
| Slice_to_incl _
| Slice_to_excl
) => #minval[T]
| (Slice_from i
| Slice_from_counted (i,_)
| Slice_range_incl (i,_)
| Slice_range_excl (i,_)
| Slice_one i
) => i
| Slice_none => #maxval[T]
;
fun max[T with BoundRandomSequence[T]] (x:slice[T]) => match x with
| ( Slice_all
| Slice_from _
) => #maxval[T]
| Slice_from_counted (i,n) => pred (advance (n, i))
| Slice_to_incl i => i
| Slice_to_excl i => pred i
| Slice_range_incl (_,i) => i
| Slice_range_excl (_,i) => pred i
| Slice_one i => i
| Slice_none => #minval
;
fun normalise_to_inclusive_range[T with BoundRandomSequence[T]] (x:slice[T]) =>
let l = x.min in
let u = x.max in
if l <= u then Slice_range_incl (l,u)
else Slice_none[T]
;
fun \cap[T with BoundRandomSequence[T]] (x:slice[T], y:slice[T]) =>
let l = max (min x, min y) in
let u = min (max x, max y) in
if l <= u then Slice_range_incl (l,u)
else Slice_none[T]
;
fun \in[T with BoundRandomSequence[T]] (x:T, s:slice[T]) =>
match s with
| #Slice_all => true
| Slice_from i => x >= i
| Slice_from_counted (i,n) => x >= i and x < advance (n, i)
| Slice_to_incl j => x <= j
| Slice_to_excl j => x < j
| Slice_range_incl (i,j) => x >= i and x <= j
| Slice_range_excl (i,j) => x >= i and x < j
| Slice_one i => i == x
| Slice_none => false
;
gen iterator[T with BoundRandomSequence[T]] (s:slice[T]) =>
match s with
| Slice_one x => { yield Some x; return None[T]; }
| Slice_range_incl (first, last) => slice_range_incl first last
| Slice_range_excl (first, last) => slice_range_excl first last
| Slice_to_incl (last) => slice_range_incl #minval[T] last
| Slice_to_excl (last) => slice_range_excl #minval[T] last
| Slice_from (first) => slice_range_incl first #maxval[T]
| Slice_from_counted (first, count) => slice_from_counted first count
| #Slice_all => slice_range_incl #minval #maxval
| #Slice_none => { return None[T]; }
endmatch
;
// Note: guarrantees no overflow
// handles all cases for all integers correctly
// produces nothing if first > last
gen slice_range_incl[T with BoundRandomSequence[T]] (first:T) (last:T) () = {
var i = first;
while i < last do
yield Some i;
i = succ i;
done
if i == last perform yield Some i;
return None[T];
}
gen slice_range_excl[T with BoundRandomSequence[T]] (first:T) (limit:T) () = {
var i = first;
while i < limit do
yield Some i;
i = succ i;
done
return None[T];
}
gen slice_from_counted[T with BoundRandomSequence[T]] (first:T) (count:int) () = {
var k = count;
while k > 0 do
yield Some (advance (count - k, first));
k = k - 1;
done
return None[T];
}
// hack so for in f do .. done will work too
gen iterator[t] (f:1->opt[t]) => f;
// slice index calculator
// Given length n, begin b and end e indicies
// normalise so either 0 <= b <= e <= n or m = 0
//
// if m = 0 ignore b,e and use empty slice
// otherwise return a slice starting at b inclusive
// and ending at e exclusive, length m > 0
// Normalised form allows negative indices.
// However out of range indices are trimmed back:
// the calculation is NOT modular.
fun cal_slice (n:int, var b:int, var e:int) = {
if b<0 do b = b + n; done
if b<0 do b = 0; done
if b>=n do b = n; done
// assert 0 <= b <= n (valid index or one past end)
if e<0 do e = e + n; done
if e<0 do e = 0; done
if e>=n do e = n; done
// assert 0 <= e <= n (valid index or one pas end)
var m = e - b;
if m<0 do m = 0; done
// assert 0 <= m <= n (if m > 0 then b < e else m = 0)
return b,e,m;
// assert m = 0 or 0 <= b <= e <= n and 0 < m < n
}
variant gslice[T] =
| GSlice of slice[T]
| GSSList of list[gslice[T]]
| GSIList of list[T]
| GSIter of 1 -> opt[T]
| GSMap of (T -> T) * gslice[T]
;
gen gslist_iterator[T with Integer[T]] (ls: list[gslice[T]]) () : opt[T] =
{
var current = ls;
next:>
match current with
| #Empty => return None[T];
| Cons (gs, tail) =>
for v in gs do yield Some v; done
current = tail;
goto next;
endmatch;
}
gen gsmap_iterator[T] (f:T->T) (var gs:gslice[T]) () : opt[T] =
{
for v in gs do yield v.f.Some; done
return None[T];
}
gen iterator[T with Integer[T]] (gs:gslice[T]) =>
match gs with
| GSlice s => iterator s
| GSSList ls => gslist_iterator ls
| GSIList ls => iterator ls
| GSIter it => it
| GSMap (f,gs) => gsmap_iterator f gs
;
fun +[T with Integer[T]] (x:gslice[T], y:gslice[T]) =>
GSSList (list (x,y))
;
fun +[T with Integer[T]] (x:gslice[T], y:slice[T]) =>
x + GSlice y
;
fun +[T with Integer[T]] (x:slice[T], y:gslice[T]) =>
GSlice x + y
;
fun +[T with Integer[T]] (x:slice[T], y:slice[T]) =>
GSlice x + GSlice y
;
fun map[T with Integer[T]] (f:T->T) (gs:gslice[T]) =>
GSMap (f,gs)
;
}
Operations on sums of units¶
Treated as finite cyclic groups.
//[unitsum.flx]
// -----------------------------------------------------------------------------
typedef void = 0;
typedef unit = 1;
instance Str[void] {
fun str (x:void) => "void";
}
open Show[void];
instance Str[unit] {
fun str (x:unit) => "()";
}
open Show[unit];
instance[T:UNITSUM] Eq[T] {
fun == (x:T,y:T) => caseno x ==caseno y;
}
instance[T:UNITSUM] Tord[T] {
fun < (x:T,y:T) => caseno x < caseno y;
}
instance[T:UNITSUM] ForwardSequence[T] {
fun succ (x:T) => (caseno x + 1) :>> T;
}
instance[T:UNITSUM] BidirectionalSequence[T] {
fun pred (x:T) => (caseno x - 1) :>> T;
}
instance[T:UNITSUM] UpperBoundTotalOrder[T] {
fun maxval () => (memcount[T].int - 1) :>> T;
}
instance[T:UNITSUM] LowerBoundTotalOrder[T] {
fun minval () => 0 :>> T;
}
instance[T:UNITSUM] RandomSequence[T] {
fun advance (amt: int, pos:T) => (caseno pos + amt) :>> T;
}
open[T:UNITSUM] BoundRandomSequence[T];
typedef fun n"`+" (x:UNITSUM,y:UNITSUM):UNITSUM => _typeop ("_unitsum_add",(x,y),UNITSUM);
typedef fun n"`-" (x:UNITSUM,y:UNITSUM):UNITSUM => _typeop ("_unitsum_diff",(x,y),UNITSUM);
typedef fun n"`*" (x:UNITSUM,y:UNITSUM):UNITSUM => _typeop ("_unitsum_mul",(x,y),UNITSUM);
typedef fun n"`/" (x:UNITSUM,y:UNITSUM):UNITSUM => _typeop ("_unitsum_div",(x,y),UNITSUM);
typedef fun n"`%" (x:UNITSUM,y:UNITSUM):UNITSUM => _typeop ("_unitsum_mod",(x,y),UNITSUM);
typedef fun n"_unitsum_min" (x:UNITSUM,y:UNITSUM):UNITSUM => _typeop ("_unitsum_min",(x,y),UNITSUM);
typedef fun n"_unitsum_max" (x:UNITSUM,y:UNITSUM):UNITSUM => _typeop ("_unitsum_max",(x,y),UNITSUM);
typedef fun n"_unitsum_gcd" (x:UNITSUM,y:UNITSUM):UNITSUM => _typeop ("_unitsum_gcd",(x,y),UNITSUM);
typedef fun n"_unitsum_lcm" (x:UNITSUM,y:UNITSUM):UNITSUM => _typeop ("_unitsum_lcm",(x,y),UNITSUM);
typedef fun n"`<" (x:UNITSUM,y:UNITSUM):BOOL=> _typeop ("_unitsum_lt",(x,y),BOOL);
typedef fun n"`>" (x:UNITSUM,y:UNITSUM):BOOL=> _typeop ("_unitsum_lt",(y,x),BOOL);
typedef fun n"`==" (x:UNITSUM,y:UNITSUM):BOOL=> x `< y and y `< x;
// —————————————————————————–
Category Theoretic Functional Operations¶
//[functional.flx]
//$ 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)
;
//$ series reverse composition (2 functions)
fun \cdot[u,v,w] (f:u->v, g:v->w) : u -> w =>
fun (x:u) => g (f x)
;
}
Tuples¶
//[tuple.flx]
//------------------------------------------------------------------------------
// Class Str: convert to string
// Tuple class for inner tuple listing
class Tuple[U] {
virtual fun tuple_str (x:U) => str x;
}
instance[U,V with Str[U], Tuple[V]] Tuple[U ** V] {
fun tuple_str (x: U ** V) =>
match x with
| a ,, b => str a +", " + tuple_str b
endmatch
;
}
instance[U,V with Str[U], Str[V]] Tuple[U * V] {
fun tuple_str (x: U * V) =>
match x with
| a , b => str a +", " + str b
endmatch
;
}
// actual Str class impl.
instance [U, V with Tuple[U ** V]] Str[U ** V] {
fun str (x: U ** V) => "(" + tuple_str x +")";
}
instance[T,U] Str[T*U] {
fun str (t:T, u:U) => "("+str t + ", " + str u+")";
}
instance[T] Str[T*T] {
fun str (t1:T, t2:T) => "("+str t1 + ", " + str t2+")";
}
open[U, V with Tuple[U **V]] Str [U**V];
open[U, V with Str[U], Str[V]] Str [U*V];
//------------------------------------------------------------------------------
// Class Eq: Equality
instance [T,U with Eq[T], Eq[U]] Eq[T ** U] {
fun == : (T ** U) * (T ** U) -> bool =
| (ah ,, at) , (bh ,, bt) => ah == bh and at == bt;
;
}
instance[t,u with Eq[t],Eq[u]] Eq[t*u] {
fun == : (t * u) * (t * u) -> bool =
| (x1,y1),(x2,y2) => x1==x2 and y1 == y2
;
}
instance[t with Eq[t]] Eq[t*t] {
fun == : (t * t) * (t * t) -> bool =
| (x1,y1),(x2,y2) => x1==x2 and y1 == y2
;
}
//------------------------------------------------------------------------------
// Class Tord: Total Order
instance [T,U with Tord[T], Tord[U]] Tord[T ** U] {
fun < : (T ** U) * (T ** U) -> bool =
| (ah ,, at) , (bh ,, bt) => ah < bh or ah == bh and at < bt;
;
}
instance[t,u with Tord[t],Tord[u]] Tord[t*u] {
fun < : (t * u) * (t * u) -> bool =
| (x1,y1),(x2,y2) => x1 < x2 or x1 == x2 and y1 < y2
;
}
instance[t with Tord[t]] Tord[t*t] {
fun < : (t * t) * (t * t) -> bool =
| (x1,y1),(x2,y2) => x1 < x2 or x1 == x2 and y1 < y2
;
}
open [T,U with Tord[T], Tord[U]] Tord[T ** U];
open [T,U with Tord[T], Tord[U]] Tord[T * U];
open [T with Tord[T]] Tord[T * T];
/* type equality now requires type_eq!
//------------------------------------------------------------------------------
// Generic Field access
fun field[n,t,u where n==0] (a:t,b:u)=>a;
fun field[n,t,u where n==1] (a:t,b:u)=>b;
fun field[n,t,u,v where n==0] (a:t,b:u,c:v)=>a;
fun field[n,t,u,v where n==1] (a:t,b:u,c:v)=>b;
fun field[n,t,u,v where n==2] (a:t,b:u,c:v)=>c;
fun field[n,t,u,v,w where n==0] (a:t,b:u,c:v,d:w)=>a;
fun field[n,t,u,v,w where n==1] (a:t,b:u,c:v,d:w)=>b;
fun field[n,t,u,v,w where n==2] (a:t,b:u,c:v,d:w)=>c;
fun field[n,t,u,v,w where n==3] (a:t,b:u,c:v,d:w)=>d;
fun field[n,t,u,v,w,x where n==0] (a:t,b:u,c:v,d:w,e:x)=>a;
fun field[n,t,u,v,w,x where n==1] (a:t,b:u,c:v,d:w,e:x)=>b;
fun field[n,t,u,v,w,x where n==2] (a:t,b:u,c:v,d:w,e:x)=>c;
fun field[n,t,u,v,w,x where n==3] (a:t,b:u,c:v,d:w,e:x)=>d;
fun field[n,t,u,v,w,x where n==4] (a:t,b:u,c:v,d:w,e:x)=>e;
*/
//------------------------------------------------------------------------------
open class parallel_tuple_comp
{
//$ parallel composition
// notation: f \times g
fun ravel[u1,u2,r1,r2] (f1:u1->r1,f2:u2->r2) : u1 * u2 -> r1 * r2 =>
fun (x1:u1,x2:u2) => f1 x1, f2 x2;
fun ravel[u1,u2,u3,r1,r2,r3] (
f1:u1->r1,
f2:u2->r2,
f3:u3->r3
) : u1 * u2 * u3 -> r1 * r2 * r3 =>
fun (x1:u1,x2:u2,x3:u3) => f1 x1, f2 x2, f3 x3;
fun ravel[u1,u2,u3,u4,r1,r2,r3,r4] (
f1:u1->r1,
f2:u2->r2,
f3:u3->r3,
f4:u4->r4
) : u1 * u2 * u3 * u4 -> r1 * r2 * r3 * r4=>
fun (x1:u1,x2:u2,x3:u3,x4:u4) => f1 x1, f2 x2, f3 x3, f4 x4;
fun ravel[u1,u2,u3,u4,u5,r1,r2,r3,r4,r5] (
f1:u1->r1,
f2:u2->r2,
f3:u3->r3,
f4:u4->r4,
f5:u5->r5
) : u1 * u2 * u3 * u4 * u5 -> r1 * r2 * r3 * r4 * r5 =>
fun (x1:u1,x2:u2,x3:u3,x4:u4,x5:u5) => f1 x1, f2 x2, f3 x3, f4 x4, f5 x5;
}