Felix now seems to support typeclasses with enough bells,
whistles, and boxed copies of the kitchen sink, to FINALLY
allow replacement of all the grubby macros for basic C types
in the standard library with something resembling sane
high level code.
Lots of testing is needed!
BE WARNED -- not all the error messages will be sane,
and there will probably be a some cases of infinite
loops in both the compiler and runtime code if you
mess up.
///////////////////////////////////////////////////////////
//
// The first thing to do is NOT include the standard library
//
//#import <flx.flxh>
//
// Now we need some I/O to report results
//
header '#include <iostream>';
proc print[t]:t="std::cout<<$1;";
proc endl:1="std::cout<<std::endl;";
//
// and some basic definitions
//
typedef bool = 2;
typedef unit = 1;
fun lnot: 2->2 = "!$1";
typedef lvalue[t] = lval t;
//
// lift some arithmetic types from C to play with
//
ctypes short, int, long, ulong, float, double;
typedef ints = typesetof(short, int, long, ulong);
//
// A typeclass for equality
//
// Note eq,ne are defined in terms of each other
// so one of them had better be defined in every
// instance or we'll get an infinite loop at runtime
//
typeclass Eq[t] {
virtual fun eq (x:t,y:t):bool => not (ne (x,y));
virtual fun ne (x:t,y:t):bool => not (eq (x,y));
}
//
// an instance for some C integers
//
instance [t:ints] Eq[t] {
fun eq: t * t -> bool = "$1==$2";
}
// total order
typeclass Tord[t]{
inherit Eq[t];
virtual fun lt: t * t -> bool;
virtual fun gt(x:t,y:t):bool =>lt(y,x);
virtual fun le(x:t,y:t):bool => not (gt(x,y));
virtual fun ge(x:t,y:t):bool => not (lt(x,y));
}
instance[t:ints] Tord[t]{
fun lt: t * t -> bool = "$1<$2";
}
//
// additive symmetric group
//
// This typeclass includes a semantic specification!
//
typeclass Addgrp[t] {
inherit Eq[t];
virtual fun zero: 1 -> t;
virtual fun add: t * t -> t;
virtual fun inv: t -> t;
virtual fun sub(x:t,y:t):t => add (x,inv y);
virtual proc pluseq (x:lvalue[t],y:t){ x = x + y; }
virtual proc minuseq (x:lvalue[t],y:t){ x = x - y; }
reduce id (x:t): x+zero() => x;
reduce id (x:t): zero()+x => x;
axiom assoc (x:t,y:t,z:t): (x+y)+z == x+(y+z);
reduce inv(x:t): x-x => zero();
reduce inv(x:t,y:t): x+y-y => x;
axiom sym (x:t,y:t): x+y == y+x;
}
// integers form a group under addition, at least locally
instance[t:ints] Addgrp[t] {
fun zero: 1 -> t = "0" ;
fun add: t * t -> t = "$1+$2" ;
fun inv: t -> t = "-$1" ;
fun sub: t * t -> t = "$1-$2" ;
proc pluseq: lvalue[t] * t = "$1+=$2;";
proc minuseq: lvalue[t] * t = "$1-=$2;";
}
//
// A multiplicative semi-group with unit
//
// Similar to a group, but lacking an inverse,
// it does have a cancellation law instead
// (0 has no inverse)
//
typeclass MultSemi1[t] {
inherit Eq[t];
virtual fun one: unit -> t;
virtual fun mul: t * t -> t;
virtual proc muleq: lvalue[t] * t;
reduce id (x:t): x*one() => x;
reduce id (x:t): one()*x => x;
axiom assoc (x:t,y:t,z:t): (x*y)*z == x*(y*z);
reduce cancel (x:t,y:t,z:t): x * z == y * z => x == y;
}
// integers form a semi-group under multiplication, at least locally
instance[t:ints] MultSemi1[t] {
fun one: unit -> t = "1" ;
fun mul: t * t -> t = "$1*$2" ;
proc muleq: lvalue[t] * t = "$1*=$2;";
}
//
// A ring (with unit) is an additive group which
// is also a multiplicative semi-group
//
typeclass Ring[t] {
inherit Addgrp[t];
inherit MultSemi1[t];
axiom distrib (x:t,y:t,z:t): x * ( y + z) == x * y + x * z;
}
instance[t:ints] Ring[t] {}
//
// A division ring is a ring with unit which
// also supports division, except by 0
// [Note the bug: the precondition on 'div' cannot
// be stated except in a comment: this is mainly
// a syntax issue]
//
typeclass Dring[t] {
inherit Ring[t];
virtual fun div: t * t -> t; // pre t != 0
virtual proc diveq: lvalue[t] * t;
virtual fun mod : t * t -> t;
virtual proc modeq: lvalue[t] * t;
}
//
// and of course integers form a division ring
//
instance[t:ints] Dring[t] {
fun div: t * t -> t = "$1/$2" ;
proc diveq: lvalue[t] * t = "$1/=$2;";
fun mod : t * t -> t = "$1%$2" ;
proc modeq: lvalue[t] * t = "$1%=$2;";
}
//
// now define some functions depending on
// these typeclasses
//
fun g[t with Tord[t]] (x:t,y:t) => x >= y;
fun f[t with Dring[t], Eq[t]] (x:t,y:t) => x+y-y == x;
//
// and test them with arguments which are ints
//
print$ g(1,2); endl;
print$ f(1,2); endl;
//
// finally check we can just open these things
//
{
open Addgrp[int];
val x = 10;
val y = 42;
print$ x+y-y; endl;
};
{
open Dring[long];
val x = 10L;
val y = 42L;
print$ x+y-y; endl;
};
//////////////////////////////////////////////////////////
In the above code a lot of highly sophisticated work
is being done!
You will note the use of 'specialisation views', binding
of typeclass instances to typeclasses, and constraint
checking -- not to mention real, executable semantics
for our ADTs which hopefully will be amenable to
proof and optimisation opportunities.
--
John Skaller <skaller at users dot sf dot net>
Felix, successor to C++: http://felix.sf.net
-------------------------------------------------------------------------
Using Tomcat but need to do more? Need to support web services, security?
Get stuff done quickly with pre-integrated technology to make your job easier
Download IBM WebSphere Application Server v.1.0.1 based on Apache Geronimo
http://sel.as-us.falkag.net/sel?cmd=lnk&kid=120709&bid=263057&dat=121642
_______________________________________________
Felix-language mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/felix-language
