Version française
Home     About     Download     Resources     Contact us    
Browse thread
variables in 'let rec'
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: -- (:)
From: David Chemouil <David.Chemouil@e...>
Subject: variables in 'let rec'

hi


I'm currently writing a program where I need to create both variables
and functions in a 'let rec'. The problem is that it is not allowed to
define a simple variable (i.e not a variant) in a 'let rec', because it
would be able to write things such as:

# let rec x = x+1;;
This kind of expression is not allowed as right-hand side of `let rec'

This error message seems okay to me.

However, the error message also occurs in situations where there is no
problem:

# let rec x = fact 5    (* using usual fact *)
              ^^^^^^
  and even = function
  | 0 -> true
  | n -> odd (n-1)
  and odd = function
  | 1 -> true
  | n -> even (n-1);;
This kind of expression is not allowed as right-hand side of `let rec'

What is "funny" is that it is possible to write 'Some (fact 5)'...

I wonder, then, if it would be possible to be a little less strict in
the typing policy. I believe however that it must be hard to perform
this, because it believe it is undecidable in the general case. But
isn't it possible to find a less strict policy which remains decidable?
For example, what if, in the typer, the 'let rec ... and ...' definition
was split in two parts: 
- the first part would be typed first: it would contain the variable
definitions which would be typed as a normal 'let ... and ...'.
- the second part would be typed as the current 'let rec ... and ...',
but the environment would contain the variables typed in the first part.

This system would enable to create variables in a 'let rec', but would
still forbid :
- to define mutually recursive variables
- to define non-recursive functions within a 'let rec'.


Of course, I guess the problem must be harder than that, but I think the
current system isn't completely "natural", as it forbids something that
is mathematically correct... 

Anyway, if this problem is really to complex, or undecidable, or not
worth the effot, why not allow any variable definition in a 'let rec'
and print a warning message? Then, the programmer would decide if the
definition may lead to an error...


regards

dc

-- 
David Chemouil [mailto:chemouil@enseeiht.fr] [mobile: 06 84 16 26 65]

Laboratoire d'informatique et de mathématiques appliquées (IRIT-INPT)