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];

/* 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;

}