Commuting labeled arguments

Philippe Veber
 Martin Jambon
[
Home
]
[ Index:
by date

by threads
]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
Date:   (:) 
From:  Martin Jambon <martin.jambon@e...> 
Subject:  Re: [Camllist] Commuting labeled arguments 
Philippe Veber wrote: > Hi all, > > is this behaviour of the type checker expected ? > > Objective Caml version 3.11.0 > > # let f g x y = g ~x ~y;; > val f : (x:'a > y:'b > 'c) > 'a > 'b > 'c = <fun> > # let g ~y ~x = x + y;; > val g : y:int > x:int > int = <fun> > # f g;; > Error: This expression has type y:int > x:int > int > but is here used with type x:'a > y:'b > 'c > > If so, I'm tempted to fill a report to mantis anyway, to get this said > in the manual (i've not seen anything for this case, but i might have > missed something). Imagine that any function has a unique runtime representation that only accepts one particular order for its arguments. Labeled arguments can only commute during function application when a particular order is expected. Reordering is done solely by the compiler based on the presence labels. If no particular order is expected (g ~x ~y in your definition of f), then the type checker assumes something reasonable but must make a choice. This is why the first argument of f is inferred to have type (x:'a > y:'b > 'c) although a type annotation could change this. I find this interesting: # let f g x y = g ~x ~y + g ~y ~x ;; Characters 2627: g ~x ~y + g ~y ~x ^ This function is applied to arguments in an order different from other calls. This is only allowed when the real type is known. # let f (g : x:_ > y:_ > _) x y = g ~x ~y + g ~y ~x ;; val f : (x:'a > y:'b > int) > 'a > 'b > int = <fun> Martin  http://mjambon.com/