ExpandCollapsePrev Next Index

+ 3.1 Type classes

The class and instance is the primary organisation tool for Felix libraries that allow easy use and extension. The notion is taken from Haskell, generalised to support multiple type variables as in GHC.

Here is a simple typeclass and instance:

  class X[T] {
    virtual fun f: T -> T;
    fun g(x:T)=> f (f x);
  }
  
  instance X[int] {
    fun f(x:int)=> x + 1;
  }
  
  open X[int];
  
  println$ g 1;

In this code virtual functions are ones which may be overridden in instances. virtual functions may have definitions, which are used in any instance which does not define an override. Non-virtual functions cannot be overriden: instead they're dependent on the virtual functions only.

We define an instance of X for type int and then call the non-virtual function g for specialisation T -> int, which in turn calls f for that specialisation too.

Finally we open the typeclass for the specialisation T -> int. In effect this just makes f of (int) and g of (int) available.

+ 3.1.1 Orders

We will cite one of the most important typeclasses in Felix:

std/algebra/equiv.flx
  #line 266 "/home/travis/build/felix-lang/felix/src/packages/algebra.fdoc"
  // equality: technically, equivalence relation
  class Eq[t] {
    virtual fun == : t * t -> bool;
    virtual fun != (x:t,y:t):bool => not (x == y);
  
    axiom reflex(x:t): x == x;
    axiom sym(x:t, y:t): (x == y) == (y == x);
    axiom trans(x:t, y:t, z:t): x == y and y == z implies x == z;
  
    fun eq(x:t, y:t)=> x == y;
    fun ne(x:t, y:t)=> x != y;
    fun \(\ne\)(x:t, y:t)=> x != y;
    fun \(\neq\)(x:t, y:t)=> x != y;
  }
  
std/algebra/partialorder.flx
  #line 310 "/home/travis/build/felix-lang/felix/src/packages/algebra.fdoc"
  // partial order
  class Pord[t]{
    inherit Eq[t];
    virtual fun \(\subset\): t * t -> bool;
    virtual fun \(\supset\)(x:t,y:t):bool =>y \(\subset\) x;
    virtual fun \(\subseteq\)(x:t,y:t):bool => x \(\subset\) y or x == y;
    virtual fun \(\supseteq\)(x:t,y:t):bool => x \(\supset\) y or x == y;
  
    fun \(\subseteqq\)(x:t,y:t):bool => x \(\subseteq\) y;
    fun \(\supseteqq\)(x:t,y:t):bool => x \(\supseteq\) y;
  
    fun \(\nsubseteq\)(x:t,y:t):bool => not (x \(\subseteq\) y);
    fun \(\nsupseteq\)(x:t,y:t):bool => not (x \(\supseteq\) y);
    fun \(\nsubseteqq\)(x:t,y:t):bool => not (x \(\subseteq\) y);
    fun \(\nsupseteqq\)(x:t,y:t):bool => not (x \(\supseteq\) y);
  
    fun \(\supsetneq\)(x:t,y:t):bool => x \(\supset\) y;
    fun \(\supsetneqq\)(x:t,y:t):bool => x \(\supset\) y;
    fun \(\supsetneq\)(x:t,y:t):bool => x \(\supset\) y;
    fun \(\supsetneqq\)(x:t,y:t):bool => x \(\supset\) y;
  
    axiom trans(x:t, y:t, z:t): \(\subset\)(x,y) and \(\subset\)(y,z) implies \(\subset\)(x,z);
    axiom antisym(x:t, y:t): \(\subset\)(x,y) or \(\subset\)(y,x) or x == y;
    axiom reflex(x:t, y:t): \(\subseteq\)(x,y) and \(\subseteq\)(y,x) implies x == y;
  }
std/algebra/totalorder.flx
  #line 371 "/home/travis/build/felix-lang/felix/src/packages/algebra.fdoc"
  // total order
  class Tord[t]{
    inherit Eq[t];
    // defined in terms of <, argument order swap, and boolean negation
  
    // less
    virtual fun < : t * t -> bool;
    fun lt (x:t,y:t): bool=> x < y;
    fun \(\lt\) (x:t,y:t): bool=> x < y;
    fun \(\lneq\) (x:t,y:t): bool=> x < y;
    fun \(\lneqq\) (x:t,y:t): bool=> x < y;
  
  
    axiom trans(x:t, y:t, z:t): x < y and y < z implies x < z;
    axiom antisym(x:t, y:t): x < y or y < x or x == y;
    axiom reflex(x:t, y:t): x < y and y <= x implies x == y;
    axiom totality(x:t, y:t): x <= y or y <= x;
  
  
    // greater
    fun >(x:t,y:t):bool => y < x;
    fun gt(x:t,y:t):bool => y < x;
    fun \(\gt\)(x:t,y:t):bool => y < x;
    fun \(\gneq\)(x:t,y:t):bool => y < x;
    fun \(\gneqq\)(x:t,y:t):bool => y < x;
  
    // less equal
    fun <= (x:t,y:t):bool => not (y < x);
    fun le (x:t,y:t):bool => not (y < x);
    fun \(\le\) (x:t,y:t):bool => not (y < x);
    fun \(\leq\) (x:t,y:t):bool => not (y < x);
    fun \(\leqq\) (x:t,y:t):bool => not (y < x);
    fun \(\leqslant\) (x:t,y:t):bool => not (y < x);
  
  
    // greater equal
    fun >= (x:t,y:t):bool => not (x < y);
    fun ge (x:t,y:t):bool => not (x < y);
    fun \(\ge\) (x:t,y:t):bool => not (x < y);
    fun \(\geq\) (x:t,y:t):bool => not (x < y);
    fun \(\geqq\) (x:t,y:t):bool => not (x < y);
    fun \(\geqslant\) (x:t,y:t):bool => not (x < y);
  
    // negated, strike-through
    fun \(\ngtr\) (x:t,y:t):bool => not (x < y);
    fun \(\nless\) (x:t,y:t):bool => not (x < y);
  
    fun \(\ngeq\) (x:t,y:t):bool => x < y;
    fun \(\ngeqq\) (x:t,y:t):bool => x < y;
    fun \(\ngeqslant\) (x:t,y:t):bool => x < y;
  
    fun \(\nleq\) (x:t,y:t):bool => not (x <= y);
    fun \(\nleqq\) (x:t,y:t):bool => not (x <= y);
    fun \(\nleqslant\) (x:t,y:t):bool => not (x <= y);
  
  
    // maxima and minima
    fun max(x:t,y:t):t=> if x < y then y else x endif;
    fun \(\vee\)(x:t,y:t) => max (x,y);
  
    fun min(x:t,y:t):t => if x < y then x else y endif;
    fun \(\wedge\)(x:t,y:t):t => min (x,y);
  
  
  }
  

This library file defines the concept of equality, total ordering, and the core operations of integral kinds: increment and decrement.

The code shows clearly the use of axioms to express semantics, for example we see equality must be an equivalence relation (reflexive, symmetric and transitive).

Also we note that the total order concept is derived from equality concept. When you open a Tord you get the methods of Eq as well.

+ 3.1.2 Relation to C++

Type classes actually exist in much the same form in C++. If you define a template class with all static functions, then those functions without definitions are Felix virtuals, those with definitions are either non-virtuals or virtuals with defaults (C++ doesn't distinguish these two cases).

In C++, an instance is just a partical or full specialisation of the class, which in turn may include some or all of the functions. It's acceptable in both C++ and Felix to leave out definitions for functions you do not use.

The principal difference between Felix and C++ is that the C++ type system cannot support type recursion and hence is effectively useless: you cannot make a combinatorial definition of a polymorphic linked list in C++, in Felix it is a one liner:

  union list[T] = | #Empty | Cons of T * list[T];

using Felix's built in tuple and union constructors. The equivalent templates are easy to define in C++: the problem is the list[T] at the end of the definition.