FIML V0.4 Manual

Installation. Syntax. Toplevel. Primitives. Errors. Examples. Bugs. About.

Here is a short manual for the version 0.4. Contrasting with version 0.3, you can see the new syntax, and particularly the emphasis on reverse application, and abstraction-application mixing. Pooled references are another goodie.

There is an introductory sample session.

1. Installation

You can install FIML V0.4 in two ways: using caml-light batch compiler, or the interactive toplevel. On Macintoshes, only the second option is available. Caml-light V0.5 or more is necessary.

For batch compilation, just do make in the distribution directory. You then get an executable fiml, which you can move anywhere in your execution path. Just remember that when you are loading programs into FIML, the default directory is the one you were before starting.

Using FIML on top of Caml-light's toplevel is no more complicated. Start CAML.

>       Caml Light version 0.6

If this is the first time you use it, compile it by loading
- : unit = ()
- : unit = ()
You will have some warnings for

To load compiled code, just use, or to load from the sources, and call the fiml function.

- : unit = ()
- : unit = ()
Bienvenue dans FIML-light, Version 0.4 !
An interpreter by J. Garrigue, April 1994.

If for any reason you want to go back to the CAML toplevel, use the quit function. You can go back to your original state with the fiml_top function.
#quit <> ;;
A tres bientot...
- : unit = ()
#sin 1.34;;
- : float = 0.973484541695
#fiml_top () ;;
#/973 ;;
it : <int> = <973>

2. Syntax

l ::= INT | IDENT | IDENT + INT		labels
b ::= INT | true | false | "STRING"	base values
x ::= IDENT | _				variable pattern
m ::= x | <l:m,...> | <l:m,...|x>	stream
    | (c l:m ...) | (c l:m ...|x)	constructors
    | (m :- l ...) | (m :- l ... -o l ...) restricted labels
    | (m : t)				type constraint
M ::= l:m,...; E			function case
C ::= b | IDENT | (E)			closed expression
    | <l:E',...>			stream
    | <l:E',...; E>			reverse application
E'::= C | C l:C ...			application
    | let [rec] m = E (|m=E)* in E	let definition
    | E' o E				composition
    | /l:E',...				stream
E ::= E' | \ M (|M)* | E ; E		open expression
Label abbreviations:
`l:' may be ommited when it is `1'.
`p' is equivalent to `p+0'. (Think of it as p1 if you look at the papers. Then `p+1' becomes naturally p2, etc ...)
To this we must add some short-cuts:
operators: +, -, *, /, **, <#, >#, <=, >=, ||, &&, =, !=, ^, ::
lists: [A;...;D] --> (cons A ... (cons D nil) ...),
list matching: [a;...;d|t] --> (cons a ... (cons d t) ...), [a;...;d] --> (cons a ... (cons d nil) ...),
selector macro: C.p --> <C;\<l:x|_>; x>
if-then-else: if ... then:C2 else:C3 --> (\ true; C1 | false; C2) ...
references: new_ref(p): p <- E, set_ref(p): p ! r <- E, get_ref(p): p ! r
In fact let is itself a macro for
<$:E1,...,$:En; \$:m1,...,$:mn; E>
(Type checking being done "in context", polymorphism is kept.)
Some other notations are equivalent:
E1 ; E2 and E2 o E1
<l1:E1,...> and (/l1:E1,...)
";" may be omitted before "\" or "/", when not ambiguous.
eg. /1\x/x = <1>;\x;<x> = <1>

3. Toplevel

You can evaluate either expressions or definitions. To give you an handle on the result, expressions alone are in fact interpreted as defining the identifier it.
E ;; --> let it = E ;;
let [rec] m = E and ... ;;
Type definitions use the following syntax:
type [v;...] = c <l:t,...> (| c <l:t,...>)* ;;
v ::= 'a | @a | $a 	generic, return and row variables
r ::= $a | <l:t,...> | <l:t ... ;$a>	row types
w ::= @a | r | c_0 | [v;...] c_n	return types
t ::= 'a | w | r -o w			types
There is a number of toplevel pragmas:
#dialogue true ;;
sets the dialogue mode:
"E;;" is the interpreted as "it ; E;;"
#set e ;;
resets the value assigned to it
#show e ;;
shows the value of an expression
#dialogue false ;;
back to standard mode

4. Primitives and pragmas

add,sub,mult,div,mod,pow : <1:int,2:int> -o int
lt,gt,le,ge : <1:int,2:int> -o bool
or,and* : <1:bool,2:bool> -o bool
eq,neq : <1:@a,2:@a> -o bool
concat : <1:string,2:string> -o string
(*) && exist only as infix
open_std : <1:<>> -o <#std:<>>
close_std : <#std:<>> -o <>
put : <1:string,#std:<>> -o <#std:<>>
get : <#std:<>> -o <1:string,#std:<>>
Pooled references:
new_ref(p) : <'a,p:['a;$b]pool> -o <$b ref,p:['a;$b]pool>
set_ref(p) : <$b ref,'a,p:['a;$b]pool> -o <p:['a;$b]pool>
get_ref(p) : <$b ref,p:['a;$b]pool> -o <'a,p:['a;$b]pool>
nil : ['a]list = []
cons : <1:'a,2:['a]list> -o ['a]list
quit : <1:<>> -o 'a
dummy* : 'a = <>
(*) dummy is temporarily made available to deal with type-driven control mechanisms. Dangerous!

5. Error handling

6. Programming examples
Basic functions and transformations. Best to use it always.
A few other functions. Necessary for
A complete algorithm for unification, handling errors!
Other little examples.
Some classical types.
Fundamental combinators of the transformation calculus.
Some definitions to handle binary directed graphs using pooled references.

7. Bugs and future developments

The only known practical bug is erroneous line numbers in error messages. But there are many theoretical ones.

In fact, there are no simple solutions to many typing problems in FIML. It results in leaving a terrible hole as the dummy untyped constant. It lets you do anything you want, and may even result in an uncaught error if you use it to induce the type-checker into error.

Even not going as far as that, the current type system does not guarantee unicity of encapsulated states. It is possible to achieve it by a combination of existential and linear types, but prohibiting this would make the system heavier, and not so pleasant as an interactive toy.

Last, this is not really a bug, but the central position of state handling in this language suggests that it should at least have either a lazy or concurrent semantics. Otherwise, all this complication comparing it to ML has little meaning.

To conclude, FIML V0.5 should have a stronger type-checking, and use lazy evaluation. And, if the theory progresses enough, even some object-oriented features.

8. About the transformation calculus and its typing

For the typing of selective lambda-calculus, a subset of the transformation calculus, see [1].

For transformation calculus, [3] gives its definition and [2] adds to it with simple typing and a glimpse of polymorphism. The best way to understand it is certainly to try this interpreter.

These papers can be found on or through the WWW.

  1. The typed polymorphic label-selective lambda-calculus. Jacques Garrigue and Hassan Aït-Kaci. In Proc. ACM Symposium on Principles of Programming Languages, pages 35-47, 1994. abstract.
  2. Transformation calculus and its typing. Jacques Garrigue. In Proc. of the workshop on Type Theory and its Applications to Computer Systems, pages 34-45. Kyoto University RIMS Lecture Notes 851, August 1993. abstract.
  3. The Transformation Calculus. Jacques Garrigue. Technical Report TR 94-09, Department of Information Science, the University of Tokyo, April 1994. abstract.

JG 94.6.10