Typing problem

Typing problem

[Daniel Bünzli]

Hello,

I would like to define the following types.

> type u = [ `U1 | `U2 ]
>
> type 'a t = [`A of 'a | `B of ([`U1 ] as 'a) ] constraint 'a = [< u ]

t's parameter is used to statically express constraints in other  
parts of the code. My problem is that
the constraint on 'a is downgraded to [`U1] while I would like to be  
able to write

> let param : 'a t -> 'a = function (`A v | `B v) -> v

and get the following typing behaviour.

> let v = param (`A `U1) (* should type *)
> let v = param (`A `U2) (* should type *)
> let v = param (`B `U1) (* should type *)
> let v = param (`B `U2) (* should not type *)

Is it possible to express that in ocaml's type system ?

Regards,

Daniel

Re: [Caml-list] Typing problem

[Jacques Garrigue]

From: Daniel Bünzli <daniel.buenzli@epfl.ch>

> I would like to define the following types.
> 
> > type u = [ `U1 | `U2 ]
> >
> > type 'a t = [`A of 'a | `B of ([`U1 ] as 'a) ] constraint 'a = [< u ]
> 
> t's parameter is used to statically express constraints in other  
> parts of the code. My problem is that
> the constraint on 'a is downgraded to [`U1]

Indeed. Constraints are shared in the whole type, so if 'a has two
 occurences in the type they represent the same type.

> while I would like to be able to write
> 
> > let param : 'a t -> 'a = function (`A v | `B v) -> v
> 
> and get the following typing behaviour.
> 
> > let v = param (`A `U1) (* should type *)
> > let v = param (`A `U2) (* should type *)
> > let v = param (`B `U1) (* should type *)
> > let v = param (`B `U2) (* should not type *)
> 
> Is it possible to express that in ocaml's type system ?

For the above definition of param, this is clearly impossible: a
single variable can have only one (polymorphic) type.
Depending on your concrete problem, there may be a way to encode it in
the type system, but not along the lines you describe here, which are
strongly reminiscent of GADTs.

For instance:
module M : sig
  type 'a t = private [< `A of 'a | `B of 'a]
  val a : ([< `U1 | `U2 ] as 'a) -> 'a t
  val b : [ `U1 ] -> [ `U1 ] t
end = struct
  type 'a t = [`A of 'a | `B of 'a]
  let a x = `A x
  let b x = `B x
end
let param : 'a M.t -> 'a = function (`A v | `B v) -> v

The properties you describe are guaranteed, because all values must be
created through M.a and M.b.

Hope this helps.

Jacques Garrigue

Re: [Caml-list] Typing problem

[Daniel Bünzli]

Le 19 mars 06 à 12:21, Jacques Garrigue a écrit :

> The properties you describe are guaranteed, because all values must be
> created through M.a and M.b.

I thought about that but I wanted to avoid the need to go through  
constructors functions (or values à la bigarray). Maybe I'll simply  
statically check a little less. It's a tradeoff.


Le 19 mars 06 à 15:23, j h woodyatt a écrit :

> However, 'b is concrete in your example, so-- if it's fully  
> representative of your code-- you could just do this, and you would  
> still have only one type parameter:
>
> type 'a t = [ `A of 'a | `B of [ `U1 ] ]
>   constraint 'a = [< u ]

This won't work because, as I said, I use 'a to express static  
constraints about the value stored in the constructors therefore 'a  
must be [`U1] whenever a `B is constructed and this is not enforced  
by this definition. Having more parameters is not an option either.

Thanks to both of you for your input.

Daniel

Re: Typing problem

[j h woodyatt]

Daniel Bünzli <daniel.buenzli@epfl.ch>
>
> I would like to define the following types.
>
>> type u = [ `U1 | `U2 ]
>> type 'a t = [`A of 'a | `B of ([`U1 ] as 'a) ] constraint 'a = [< u ]
>
> t's parameter is used to statically express constraints in other  
> parts of the code. My problem is that the constraint on 'a is  
> downgraded to [`U1] while I would like to be able to write
>
>> let param : 'a t -> 'a = function (`A v | `B v) -> v
>
> and get the following typing behaviour.
>
>> let v = param (`A `U1) (* should type *)
>> let v = param (`A `U2) (* should type *)
>> let v = param (`B `U1) (* should type *)
>> let v = param (`B `U2) (* should not type *)
>
> Is it possible to express that in ocaml's type system ?

The short answer is no.  The reason is that 'a is not the same type  
in the `A case as in the `B case.  Type t really has two type  
parameters.  (Well, it can have only one if this contrived example is  
fully representative of your code, as I'll describe below).

type ('a, 'b) t = [ `A of 'a | `B of 'b ]
   constraint 'a = [< u ] constraint 'b = [ `U1 ]

However, 'b is concrete in your example, so-- if it's fully  
representative of your code-- you could just do this, and you would  
still have only one type parameter:

type 'a t = [ `A of 'a | `B of [ `U1 ] ]
   constraint 'a = [< u ]

—
j h woodyatt <jhw@conjury.org>

Re: Typing problem

[Jacques Garrigue]

From: Jean-Marc Alliot <alliot@recherche.ena.fr>
> We recently found a quite annoying problem with the typing system in
> ocaml 2.99, and Jacques Garrigue explained it to us very kindly. Other
> people might be be interested however.
> 
> The problem is summarized in the following code:
> 
> First let's define two types:
> type t1 = (?l:int -> unit -> unit)
> type t = Toto of t1
> 
> Then the function:
> let f1 g =
>   g l:3 ();
>   (Toto g);;
> 
> This function doesn't compile and the compiler error message is somewhat
> cryptic at first sight:
> File "toto.ml", line 11, characters 8-9:
> This expression has type int -> unit -> 'a but is here used with type
>   t1 = ?l:int -> unit -> unit
>
> We would very much like to see this clearly documented in ocaml 2.99
> reference manual, as it is a serious change in the behavior of the
> typing system. Determinism is lost, as typing f1 would succeed if typing
> was done in reverse order (from last line to first line).

Sorry, I overlooked this point the manual.

As Pierre pointed out, what is lost here is not determinism but
completeness. The compiler may fail to type some correct programs, but
when it gives a result this will always be the same type.

To be more precise, ocaml 2.99 added two features to function
application:

* out-of-order parameter passing (with labels)
* optional arguments

Both of these features require type information to be available at
application point. For the first one, this is only required for
efficient compilation, but for the second one type inference cannot be
done without it.

So you have to put a type annotation on g for the program to be
accepted.

# let f1 (g : t1) =
    g l:3 ();
    (Toto g);;
val f1 : t1 -> t = <fun>

The choice here has been to keep backwards compatibility: all programs
that do not use extended application will be typed. That is, by
default the compiler supposes that there are no optional arguments, and
that all arguments are in the right order.

As for the incompleteness problem, we have the theoretical foundation
to solve it. That is, we could modify the type system so as to refuse
the opposite order also, which is somehow wrongly accepted.

# let f1 g = ignore(Toto g); g l:3 ();;
val f1 : t1 -> unit = <fun>

But I'm not sure refusing such cases would help a lot in practice.
This is not done currently because this check would badly slow down
the compiler.

> Perhaps also a different error message from the compiler would help in
> detecting such problems.

The above error message tells almost all the compiler knows. That is,
you mixed an optional and a non-optional argument, which is
illegal. The non-optional label disappears in the printed type because
in classic mode it is irrelevant for unification. I believe the
problem was that you didn't know that such a problem may occur at all.

In this particular case, by analyzing the two incompatible types, we
may discover that they both use the label l:, in its optional an
non-optional forms. So, with quite a bit of work, we could also have a
message:

Optional label ?l: and non-optional label l: are incompatible.

But we must then also think about out-of-order application, omitted
parameters... Which all need a specific treatment.

Do you think this would help a lot?

From: Pierre Weis <Pierre.Weis@inria.fr>
> Hence, a language level fix could simply be to allow the user to write
> the question mark with the label as:
> 
> let f1 g =
>     g ?l:3 ();
>     (Toto g);;
> 
> Now, in conjontion with the -modern option, this would be perfectly clear to
> understand why g l:3 is rejected while g ?l:3 is not.
> 
> Unfortunately, this last program is not yet handled properly by the
> compiler, since it causes an assertion failure into the typechecker:
> 
> # let f1 g =
>       g ?l:3 ();
>       (Toto g);;
> This expression has type ?l:Uncaught exception: File
> "typing/printtyp.ml", line 0, characters 6649-6661: Assertion failed

In fact, this feature is already available in ocaml 2.99. However the
above program is ill-typed, and due to a hole in the type checker,
some invalid type expression makes the pretty printer crash.

With a corrected version of the compiler, you get the following error
message.
# let f1 g =
        g ?l:3 ();
             ^
        (Toto g);;  
This expression has type int but is here used with type 'a option

That is, using a question mark in an application is symmetrical to
abstraction, and you must provide an optional value (of type int
option here). This feature is documented in the reference manual.

# let f1 g =
    g ?l:(Some 3) ();
    (Toto g);;
val f1 : t1 -> t = <fun>

This only solves half of the problem, since you still have to pass all
arguments (included omitted ones), and in the right order.

Regards,

Jacques
---------------------------------------------------------------------------
Jacques Garrigue      Kyoto University     garrigue at kurims.kyoto-u.ac.jp
		<A HREF=http://wwwfun.kurims.kyoto-u.ac.jp/~garrigue/>JG</A>

Re: Typing problem

[Pierre Weis]

> We recently found a quite annoying problem with the typing system in
> ocaml 2.99, and Jacques Garrigue explained it to us very kindly. Other
> people might be be interested however.
> 
> The problem is summarized in the following code:
> 
> First let's define two types:
> type t1 = (?l:int -> unit -> unit)
> type t = Toto of t1
> 
> Then the function:
> let f1 g =
>   g l:3 ();
>   (Toto g);;
> 
> This function doesn't compile and the compiler error message is somewhat
> cryptic at first sight:
> File "toto.ml", line 11, characters 8-9:
> This expression has type int -> unit -> 'a but is here used with type
>   t1 = ?l:int -> unit -> unit

Thank you very much for pointing out this interesting problem: I'm
sure there is room for improvement here for our new label compiler.

If you use the -modern option of the compiler you would get a much
clearer message, namely:

# let f1 g =
    g l:3 ();
    (Toto g);;
This expression has type l:int -> unit -> 'a but is here used with
type
  t1 = ?l:int -> unit -> unit

This clearly states that the optional status of the label is involved
in the problem.

Hence, a language level fix could simply be to allow the user to write
the question mark with the label as:

let f1 g =
    g ?l:3 ();
    (Toto g);;

Now, in conjontion with the -modern option, this would be perfectly clear to
understand why g l:3 is rejected while g ?l:3 is not.

Unfortunately, this last program is not yet handled properly by the
compiler, since it causes an assertion failure into the typechecker:

# let f1 g =
      g ?l:3 ();
      (Toto g);;
This expression has type ?l:Uncaught exception: File
"typing/printtyp.ml", line 0, characters 6649-6661: Assertion failed

> We would very much like to see this clearly documented in ocaml 2.99
> reference manual, as it is a serious change in the behavior of the
> typing system. Determinism is lost, as typing f1 would succeed if typing
> was done in reverse order (from last line to first line).
> Perhaps also a different error message from the compiler would help in
> detecting such problems.

I don't think that determinism is lost, in the sense that the compiler
always output the same answers! But you're right to mention that this
would be another way to test in which order in which the type-checker
type-checks the sub-expressions of a program.

You're also right in that we always would like better and better error
messages, I would say particularly for the last program I wrote: we
would very much like the compiler not to fail to print the error
report!

No doubt that this erroneous error message will be corrected before
the experimental 2.99 version will turn into a stable 3.0 version of
Objective Caml. Also, may be Jacques could tell us what is his opinion
about the optional labels status in expressions (as in g ?l:3).

Best regards,
-- 
Pierre Weis

INRIA, Projet Cristal, http://pauillac.inria.fr/~weis

Typing problem

[jean-marc alliot]

We recently found a quite annoying problem with the typing system in
ocaml 2.99, and Jacques Garrigue explained it to us very kindly. Other
people might be be interested however.

The problem is summarized in the following code:

First let's define two types:
type t1 = (?l:int -> unit -> unit)
type t = Toto of t1

Then the function:
let f1 g =
  g l:3 ();
  (Toto g);;

This function doesn't compile and the compiler error message is somewhat
cryptic at first sight:
File "toto.ml", line 11, characters 8-9:
This expression has type int -> unit -> 'a but is here used with type
  t1 = ?l:int -> unit -> unit

To make it compile, you have to type explicitly g with:
let f2 (g : t1) =
  g l:3 ();
  (Toto g);;

We would very much like to see this clearly documented in ocaml 2.99
reference manual, as it is a serious change in the behavior of the
typing system. Determinism is lost, as typing f1 would succeed if typing
was done in reverse order (from last line to first line).
Perhaps also a different error message from the compiler would help in
detecting such problems.


P Brisset
JM Alliot