Authors : erickt : May 2007
Felix 1.1.3 is Out!
posted on May 24, 2007 - 10:38 PM PDT by Erick Tryzelaar
I'm pleased to announce that version 1.1.3 of Felix has been released. Download it here. It's a substantial release and adds three major features:
Haskell-style Typeclasses
These typeclasses are analogous to C++ style templates, but are theoretically more sound. This now lets you implement typesafe constrained polymorphism. This means that you can do proper string conversion for arbitrary data, like this:
| open List; |
| typeclass Str[T] { |
| virtual fun str: T -> string; |
| } |
| instance Str[int] { fun str (x:int): string => itoa x; } |
| instance Str[string] { fun str (x:string): string => x; } |
| instance[T with Str[T]] Str[list[T]] { |
| fun str (xs:list[T]): string => |
| '[' + |
| match xs with |
| | Empty[T] => '' |
| | Cons(?o, ?os) => |
| List::fold_left ( |
| fun (a:string) (b:T): string => a + ', ' + (str b) |
| ) (str o) os |
| endmatch |
| + ']' |
| ; |
| } |
| open Str[int]; |
| open Str[string]; |
| open[T] Str[list[T]]; |
| print $ str 1; endl; |
| print $ str "hello"; endl; |
| print $ str $ list (1, 2, 3); endl; |
| print $ str $ list ("a", "b", "c"); endl; |
prints:
| 1 |
| hello |
| [1, 2, 3] |
| [a, b, c] |
First Order Axioms and Reductions
By specifying a typeclass has various axioms and reductions associated with it, felix can check if a typeclass matches certain formal specifications by testing the axioms and reductions against a small subset of values. User-specified Reductions also can assist the optimizer by saying certain patterns of code can be reduced to a simpler form. For instance, you can specify a number class can be simplified if added to zero:
| typeclass Number[T] { |
| virtual fun zero: 1 -> T; |
| virtual fun add: T * T -> T; |
| reduce identity (x:T): x + zero() => x; |
| } |
Why Code Generation
Why is a front end generator for many computer theorem provers. Instead of just using limited testing, the why code can be used in conjunction with a theorem prover to fully verify if the code does what it is supposed to do. This is an experimental feature, it does verify at least one simple lemma.
All this, along with many bug fixes and other minor improvements. Please try it out and let us know if you have any comments or run into problems.