I was playing around some more with GADTs, preparing my next course
on functional programming, and came across an example on
which the type checker outputs a type containing a funny name
for a type variable.
I do not know if this qualifies as a bug, so before filing it, I'd
love some feedback.
Here we are: I am writing an example to show how one can code
a well typed length function for empty/nonempty list; we start
with the type definition
type empty
type nonempty
type ('a, 'b) l =
Nil : (empty, 'b) l
| Cons : 'b * ('a, 'b) l -> (nonempty, 'b) l;;
then we move on to the length function
let rec length : type a b. (a,b) l -> 'a = function
| Nil -> 0
| (Cons (_,r)) -> 1+ (length r);;
Hey, you say, the natural type to declare for length should be
type a b. (a,b) l -> int
but as you see, for some mysterious reason I ended
up writing something silly (dont ask why, I am just
very well known to step on strange bugs as easily
as I breath)
type a b. (a,b) l -> 'a
The type checker is happy anyway: 'a will be instantiated
to int, and the declaration of length is accepted... but now
look at the output type
val length : ('a1, 'b) l -> int = <fun>
Why do we get 'a1, and not 'a, in the type?
Well, probably, since 'a is instantiated to int during
type checking, it may be the case that 'a, as type name, is
still marked as taken during the type output, so we get ('a1,'b)
The type is perfectly sound... it is just 'surprising' for
a regular user... do you think this should be considered a bug?
--Roberto
------------------------------------------------------------------
Professeur En delegation a l'INRIA
PPS E-mail: robe...@dicosmo.org
Universite Paris Diderot WWW : http://www.dicosmo.org
Case 7014 Tel : ++33-(0)1-57 27 92 20
5, Rue Thomas Mann
F-75205 Paris Cedex 13 Identica: http://identi.ca/rdicosmo
FRANCE. Twitter: http://twitter.com/rdicosmo
------------------------------------------------------------------
Attachments:
MIME accepted, Word deprecated
http://www.gnu.org/philosophy/no-word-attachments.html
------------------------------------------------------------------
Office location:
Bureau 6C08 (6th floor)
175, rue du Chevaleret, XIII
Metro Chevaleret, ligne 6
------------------------------------------------------------------
--
Caml-list mailing list. Subscription management and archives:
https://sympa-roc.inria.fr/wws/info/caml-list
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs
