FIML V0.4 Manual

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

There is an introductory sample session.

1. Installation

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.

%camllight
>       Caml Light version 0.6

#

#include"fimlm";;
- : unit = ()
...
- : unit = ()

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

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

#

#quit <> ;;
A tres bientot...
- : unit = ()
#sin 1.34;;
- : float = 0.973484541695
#fiml_top () ;;
#/973 ;;
it : <int> = <973>

Expressions

Basics
l ::= INT | IDENT | IDENT + INT		labels
b ::= INT | true | false | "STRING"	base values
Patterns
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
Expressions
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>

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:

load"filename";;

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

Operators:

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

I/Os:

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>

Others:

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!

• Syntax : gives you the line number and position of the error. May be erroneous.
• 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.

prelude.fm

Basic functions and transformations. Best to use it always.

prelude2.fm

A few other functions. Necessary for examples.fm.

unif.fm

A complete algorithm for unification, handling errors!

examples.fm

Other little examples.

types.fm

Some classical types.

combinators.fm

Fundamental combinators of the transformation calculus.

graph.fm

Some definitions to handle binary directed graphs using pooled references.

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 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 camille.is.s.u-tokyo.ac.jp:/pub/papers 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.