FIML V0.4 Manual
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.
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
Using FIML on top of Caml-light's toplevel is no more complicated.
> Caml Light version 0.6
If this is the first time you use it, compile it by loading fimlm.ml.
- : unit = ()
- : unit = ()
You will have some warnings for fimlfun.ml.
To load compiled code, just use fiml.ml, or fimli.ml 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
#quit <> ;;
A tres bientot...
- : unit = ()
- : float = 0.973484541695
#fiml_top () ;;
it : <int> = <973>
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:
+, -, *, /, **, <#, >#, <=, >=, ||, &&, =, !=, ^, ::
- 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>
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
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:
- loads filename.fm
- #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
- set_ref(p) : <$b ref,'a,p:['a;$b]pool> -o
- get_ref(p) : <$b ref,p:['a;$b]pool> -o
- 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
- Syntax : gives you the line number and position of the error. May
- Type-checking : gives you the internal cause of the error. This
may not always be enough. The line number is that of the end of the
definition in which the error occured , not that of the error itself.
6. Programming examples
- Basic functions and transformations.
Best to use it always.
- A few other functions. Necessary for examples.fm.
- 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
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
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
8. About the transformation calculus and its
For the typing of selective lambda-calculus, a subset of the
transformation calculus, see .
For transformation calculus,  gives its definition and  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
camille.is.s.u-tokyo.ac.jp:/pub/papers or through the WWW.
- 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.
- Transformation calculus and its typing.
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.
- The Transformation Calculus.
Jacques Garrigue. Technical Report TR 94-09, Department of
Information Science, the University of Tokyo, April 1994.