Re: bottom types and threaded exits

Re: bottom types and threaded exits

[Damien Doligez]

>From: Remi VANICAT <remi.vanicat@labri.u-bordeaux.fr>

>exception Sould_never_be_here
>
>let f () = while true do () done ; raise Sould_never_be_here

That's what "assert false" was invented for: the canonical expression
that "returns" a result of type 'a and should normally never be
evaluated.

let f () = while true do () done; assert false;;

-- Damien

Re: bottom types and threaded exits

[Pierre Weis]

> On Mon, 02 Oct 2000, Patrick M Doane wrote:
> > This may be too obvious to point out, but that statement isn't always
> > true. From the Pervasives library:
> > 
> >   val input_value : in_channel -> 'a
> > 
> > clearly returns. I don't quite understood why the return type isn't
> > a monomorphic type variable though.
> 
> The "input_value"-function is unfortunately not type safe: you can "cast"
> whatever data you get from the channel to any kind of type - whether this
> is correct or not. There is currently no better way to do it if you want to
> reconstruct marshalled data (data that was sent with output_value). You
> have to trust that the OCaml-data you get is of the type you expect.
> 
> Pierre mentioned that there is work going on in this field (a PhD-thesis)
> that should make I/O much safer. Is there any news about this?
> 
> Best regards,
> Markus Mottl
> 
> -- 
> Markus Mottl, mottl@miss.wu-wien.ac.at, http://miss.wu-wien.ac.at/~mottl

Nothing to add to Markus explanation, except that the type of (the
equivalent of) input_value in the new system is

 Forall $a. in_channel -> $a

the $ in $a meaning that this is not a regular structural polymorphic
type parameter, but a special ``dynamic'' type parameter (with special
typing rule and compilation).

Jun Furuse is working on the subject. His PhD-thesis is on the way
(more than 150 pages written). The type system and compiler are up and
running on top of a 2.99 Objective Caml system. The current plan is to
distribute this version as soon as the final draft of the thesis is
achieved, since the thesis definitively has the highest priority.

Pierre Weis

INRIA, Projet Cristal, Pierre.Weis@inria.fr, http://cristal.inria.fr/~weis/

Re: bottom types and threaded exits

[Markus Mottl]

On Mon, 02 Oct 2000, Patrick M Doane wrote:
> This may be too obvious to point out, but that statement isn't always
> true. From the Pervasives library:
> 
>   val input_value : in_channel -> 'a
> 
> clearly returns. I don't quite understood why the return type isn't
> a monomorphic type variable though.

The "input_value"-function is unfortunately not type safe: you can "cast"
whatever data you get from the channel to any kind of type - whether this
is correct or not. There is currently no better way to do it if you want to
reconstruct marshalled data (data that was sent with output_value). You
have to trust that the OCaml-data you get is of the type you expect.

Pierre mentioned that there is work going on in this field (a PhD-thesis)
that should make I/O much safer. Is there any news about this?

Best regards,
Markus Mottl

-- 
Markus Mottl, mottl@miss.wu-wien.ac.at, http://miss.wu-wien.ac.at/~mottl

Re: bottom types and threaded exits

[Patrick M Doane]

On 30 Sep 2000, Stefan Monnier wrote:

> A function of type "t1 -> t2" does not necessarily return an object of type t2.
> But if it does return, then the value is of type t2.
> Similarly, a function of type "t1 -> 'a" (if it returns) returns an value
> of type 'a.  Parametricity allows us to infer from that that if t1 does
> not contain 'a as a free type variable, then the function will necessarily
> never return (since it has no way to construct an value of
> type 'a).

This may be too obvious to point out, but that statement isn't always
true. From the Pervasives library:

  val input_value : in_channel -> 'a

clearly returns. I don't quite understood why the return type isn't
a monomorphic type variable though.

Patrick Doane

Re: bottom types and threaded exits

[Markus Mottl]

On Sat, 30 Sep 2000, Pierre Weis wrote:
> Once more I would prefer a more general recursive function, that would
> loop for any (even non looping) function. For instance:
> 
> # let rec bottom f = f (); bottom f;;     
> val bottom : (unit -> 'a) -> 'b = <fun>
> 
> and I consider the 'b in the type of bottom as clearly indicating the
> looping for ever nature of any application of the bottom function.

The name "bottom" might be a bit confusing in this context, because "f"
could be a function with observable side effects (e.g. I/O), whereas
"bottom" is usually used to indicate non-termination only, which cannot be
observed.

But this function (with a different name) and others would come handy more
often than once, e.g.:

  let rec forever f = f (); forever f
  let try_forever e f = try forever f with exn -> if e <> exn then raise exn

This would allow:

  let _ =
    try_forever End_of_file (fun () -> print_endline (read_line ()));
    print_endline "Done!"

It is much more tedious (and error-prone if one forgets the "begin ...
end") to write the following:

  let _ =
    begin
      try while true do print_endline (read_line ()) done
      with End_of_file -> ()
    end;
    print_endline "Done!"

Maybe functions similar to "forever" and "try_forever" could make it into
the standard library? Such loops come up quite often with e.g. servers or
I/O-loops in general.

Best regards,
Markus Mottl

-- 
Markus Mottl, mottl@miss.wu-wien.ac.at, http://miss.wu-wien.ac.at/~mottl

Re: bottom types and threaded exits

[Stefan Monnier]

>>>>> "Julian" == Julian Assange <proff@iq.org> writes:
> It depends on what level of semantics you are looking at. As far as
> type proofing is concerned, 'a is correct. However at a higher level
> you can say `the function never returns so saying that it returns any
> type is incorrect'. The problem is that some functions that do return,

A function of type "t1 -> t2" does not necessarily return an object of type t2.
But if it does return, then the value is of type t2.
Similarly, a function of type "t1 -> 'a" (if it returns) returns an value
of type 'a.  Parametricity allows us to infer from that that if t1 does
not contain 'a as a free type variable, then the function will necessarily
never return (since it has no way to construct an value of
type 'a).

It would maybe be a good idea to analyze the types based on a few
such parametricity-derived theorems and print a more meaningful type
(i.e. use 'noreturn rather than 'a for the above case or 'ignored
for an argument type 'a which appears only once).


        Stefan

Re: bottom types and threaded exits

[Pierre Weis]

> Xavier Leroy <Xavier.Leroy@inria.fr> writes:
> 
> > That's one way of putting it, but as Pierre Weis mentioned, fully
> > polymorphic types such as 'a appear naturally during type inference
> > for non-terminating expressions.
> 
> Yes, I found that quite cool.

Ok, but note that there is nothing special in the compiler to do so:
it is a mere consequence of the Damas-Milner typing discipline.

> > Semantically, it is correct to assign type 'a to any expression that
> > never returns normally: there are no values of type 'a, but such
> > expressions never result in a value.
> 
> It depends on what level of semantics you are looking at. As far as
> type proofing is concerned, 'a is correct. However at a higher level
> you can say `the function never returns so saying that it returns any
> type is incorrect'. The problem is that some functions that do return,
> return 'a. Ocaml's overloading of 'a, is much the same as lisps
> overloading of nil and C's overloading of 0 or void*. You might
> counter saying that 'a is defined in terms of type-unification, thus
> reading additional meaning into the type is bogus. But such a view
> denies the semantics of what is being typed. A computer language --
> one of the important semantics of which is that is capable of capable
> of generating functions that fail to return.

I think there is some misunderstanding here. The meaning of type
variables (those 'a) can be semantically quite different depending on
their binding status. This is not random stuff: it is based on
theoretical grounds, such as:

Theorem: There is no Caml value with type 'a (meaning for all 'a. 'a).

Theorem: If the target type of a function is a universally quantified
type variable that does not appear in the source type of the function,
then this function never returns: it fails to terminate or raises an
exception.

The converse property is false, since a function may loop without having
such a polymorphic type.

Examples: all of the following functions loop for ever; for some of
them this can be proved from the mere examination of their type, for
others it cannot.

# let rec f x = f x;;
val f : 'a -> 'b = <fun>

This 'b is free in the source type of f: f loops or fail.

# let rec g x = g (x + 1);;
val g : int -> 'a = <fun>

This 'a is free in the source type of g: g loops or fails.

# let rec h x = h x + 1;;
val h : 'a -> int = <fun>

This 'a is bound in the source type of h, we know that h is
polymorphic but we cannot conclude something about its termination.

# let rec i x = i (i x);;
val i : 'a -> 'a = <fun>

This 'a in the target type is bound in the source type: we cannot
conclude something about the termination of i from its type (although,
the code of i clearly fails to terminate).

# let rec j x = j (x + 1) + 1;;
val j : int -> int = <fun>

j has a regular type, we cannot conclude something about its
termination.

> `the function never returns so saying that it returns any
> type is incorrect'.

You mean for instance that the type of the preceding j function
(int -> int) is wrong since j is looping and never returns anything ?

Sorry, nobody can implement such a typing discipline due to the
well-know halting problem.

> The problem is that some functions that do return,
> return 'a.

Oversimplified and confusing. You confuse 'a type variables that are
bound in the source type of the function with 'a type variables that
are not. You should say ``some functions that do return, return 'a
that is bound into their source type'', and ``no functions that do
return, return an 'a that is unbound into their source type'' (this is
also a bit oversimplified, we should introduce the notion of positive
and negative occurrence of type variables...).

> Ocaml's overloading of 'a, is much the same as lisps
> overloading of nil and C's overloading of 0 or void*.

You should see now that there is no notion of overloading of type
variables in Caml. Nor any relationship with any nil NULL or void*
polymorphic default value.

> You might counter saying that 'a is defined in terms of
> type-unification, thus reading additional meaning into the type is
> bogus.

On the contrary, reading additional meaning into the type is a good
idea, I tried to give some simple examples in this message. But you
can use types for many more semantical properties (exceptions, safety
of programs, ...). Thus ``reading additional meaning into the type'' is
really a good idea.

> But such a view denies the semantics of what is being typed. A
> computer language -- one of the important semantics of which is that
> is capable of capable of generating functions that fail to return.

Absolutely, we do want to be able to define functions that fail to
return. That's why implementing a view such as: ``the type must tell
if the function may loop'' is hopeless, if you have general recursion in
the language. If you accept to abandon general recursion, you may
gain some much stronger typing disciplines (e.g. dependent types in
Coq) that gives you stronger properties of ``what is being types''.

> > Thread.exit should also have type unit -> 'a; the reason it currently
> > has type unit -> unit is due to the way it is implemented
> > (as Thread.kill(Thread.self())), but this is more of an historical
> > accident.
> 
> I've used:
> 
>    let exit = Thread.exit (); assert false
> 
> to get the required type. While clearly a hack, it's better to use a
> simple construct like this instead of having a casting to 'a
> mechanism. Although I find full-bown determinacy types, mercury style
> (but god forbid mercury heavy handed type syntax) quite appealing.

What do you want here:
- an exit function (then you must write let exit () = ...) ? 
- or a value of type 'a (that you cannot have in Caml, as is well-known) ?

In the first case, why not using a recursive function, such as:

let rec exit () = Thread.exit (); exit ();;
val exit : unit -> 'a = <fun>

In the second case, you will not have it. You will write an expression
that fails to return the desired value!

> > Finally, concerning "while true do e done", there is only one typing
> > rule in the type-checker for "while p do e done", which assumes that
> > "p" may become false and the loop may thus terminate with the result
> > "()", hence the "unit" type.
> 
> This is fair. I think an assert false at the end of the loop, or
> 
> let bottom f = f (); assert false
> bottom (fun () -> while true do () done)
> 
> is effective.

Once more I would prefer a more general recursive function, that would
loop for any (even non looping) function. For instance:

# let rec bottom f = f (); bottom f;;     
val bottom : (unit -> 'a) -> 'b = <fun>

and I consider the 'b in the type of bottom as clearly indicating the
looping for ever nature of any application of the bottom function.

> Although, once again, it'd be nice to see a 'bottom rather
> than 'a type come out of this, even if the two are semantically equivalent
> in the eye of the type checker.

As you may know the type parameters in type schemes are bound at the
beginning of the type scheme (prenex quantification). Hence the names
of type parameters are irrelevant. Hence 'bottom -> 'bottom and 'a ->
'a are equivalent. Anyway, we can imagine to replace negative
occurrences of type parameters that do not appear in positive
position by names that you would prefer : 'bottom, 'bottom1, 'bottom2,
etc. I don't know if the extra implementation burden is worth the
little (subliminal) additional information.

Pierre Weis

INRIA, Projet Cristal, Pierre.Weis@inria.fr, http://cristal.inria.fr/~weis/

Re: bottom types and threaded exits

[Julian Assange]

Xavier Leroy <Xavier.Leroy@inria.fr> writes:

> That's one way of putting it, but as Pierre Weis mentioned, fully
> polymorphic types such as 'a appear naturally during type inference
> for non-terminating expressions.

Yes, I found that quite cool.

> Semantically, it is correct to assign type 'a to any expression that
> never returns normally: there are no values of type 'a, but such
> expressions never result in a value.

It depends on what level of semantics you are looking at. As far as
type proofing is concerned, 'a is correct. However at a higher level
you can say `the function never returns so saying that it returns any
type is incorrect'. The problem is that some functions that do return,
return 'a. Ocaml's overloading of 'a, is much the same as lisps
overloading of nil and C's overloading of 0 or void*. You might
counter saying that 'a is defined in terms of type-unification, thus
reading additional meaning into the type is bogus. But such a view
denies the semantics of what is being typed. A computer language --
one of the important semantics of which is that is capable of capable
of generating functions that fail to return.

> Thread.exit should also have type unit -> 'a; the reason it currently
> has type unit -> unit is due to the way it is implemented
> (as Thread.kill(Thread.self())), but this is more of an historical
> accident.

I've used:

   let exit = Thread.exit (); assert false

to get the required type. While clearly a hack, it's better to use a
simple construct like this instead of having a casting to 'a
mechanism. Although I find full-bown determinacy types, mercury style
(but god forbid mercury heavy handed type syntax) quite appealing.

> Finally, concerning "while true do e done", there is only one typing
> rule in the type-checker for "while p do e done", which assumes that
> "p" may become false and the loop may thus terminate with the result
> "()", hence the "unit" type.

This is fair. I think an assert false at the end of the loop, or

let bottom f = f (); assert false
bottom (fun () -> while true do () done)

is effective. Although, once again, it'd be nice to see a 'bottom rather
than 'a type come out of this, even if the two are semantically equivalent
in the eye of the type checker.

Cheers,
Julian.

Re: bottom types and threaded exits

[Xavier Leroy]

> Pervasives.exit is of type int -> 'a
> Here we see ocaml using 'a to represent _|_. This hack is presumably
> so type unification still works in the face of potentially
> non-terminating computations

That's one way of putting it, but as Pierre Weis mentioned, fully
polymorphic types such as 'a appear naturally during type inference
for non-terminating expressions.

The prime example is recursive functions with no bottom case (let rec
f x = f (x + 1)), but raising an exception (raise Exn) also has type 'a.

Semantically, it is correct to assign type 'a to any expression that
never returns normally: there are no values of type 'a, but such
expressions never result in a value.

By the same reasoning, since a call to Pervasives.exit never returns,
it is safe and indeed logical to give it type int -> 'a.

Thread.exit should also have type unit -> 'a; the reason it currently
has type unit -> unit is due to the way it is implemented
(as Thread.kill(Thread.self())), but this is more of an historical
accident.

Finally, concerning "while true do e done", there is only one typing
rule in the type-checker for "while p do e done", which assumes that
"p" may become false and the loop may thus terminate with the result
"()", hence the "unit" type.

It would be semantically sound to give "while true do e done" the type
'a, but it would require a special type-checking rule for the "while"
construct when the predicate is "true", which sounds a bit weird.
However, we already implemented such a special case for "assert false"
(type 'a) w.r.t.  "assert cond" (type unit).

- Xavier Leroy

Re: bottom types and threaded exits

[John Prevost]

>>>>> "rv" == Remi VANICAT <remi.vanicat@labri.u-bordeaux.fr> writes:

    rv> Julian Assange <proff@iq.org> writes:
    >> Pervasives.exit is of type int -> 'a
    >> 
    >> Here we see ocaml using 'a to represent _|_. This hack is
    >> presumably so type unification still works in the face of
    >> potentially non-terminating computations, e.g:
    >> 
    >> let f a = try f a with Failure _ -> exit(1)
    >> 
    >> How can one force 'a? For instance, Thread.exit and
    >> 
    >> let f () = while true do () done
    >> 
    >> has a type of unit -> unit.
    >> 
    >> One can write something such as
    >> 
    >> let f () = while true do () done ; Pervasives.exit (1)
    >> 
    >> But this is clearly a hack.

>From what I can tell, what you're trying to do here is just make the
result type of a non-terminating computation go to 'a.  This is
actually quite easy--you just need to loop in a way that doesn't
constrain the type.  while ... do ... done always returns unit (which
is good, since usually you use it in a way that terminates.

The appropriate way to do it that will get type 'a is (in your case):

let rec f () = f ()

Note that if you choose the more direct translation

let rec f () = if true then f ()

you get constrained to type unit -> unit again, since a one-branched
if returns unit for the else branch.

So, an example of a vaguely useful function would be:

let rec call_forever f x = f x; call_forever f x

which has type:

val call_forever : ('a -> 'b) -> 'a -> 'c


So, it is not so much that 'a as bottom is a hack, as that the system
only produces such types when the result type is totally
unconstrained--and that doesn't happen with things like while loops,
only with recursion--where a function always returns the result of
calling itself (or another such function.)


John.

Re: bottom types and threaded exits

[Remi VANICAT]

Julian Assange <proff@iq.org> writes:

> Pervasives.exit is of type int -> 'a
> 
> Here we see ocaml using 'a to represent _|_. This hack is presumably
> so type unification still works in the face of potentially
> non-terminating computations, e.g:
> 
> let f a =
>         try 
>           f a
>         with
>           Failure _ -> exit(1)
> 
> How can one force 'a? For instance, Thread.exit and
> 
>         let f () = while true do () done 
> 
> has a type of unit -> unit.
> 
> One can write something such as
> 
>         let f () = while true do () done ; Pervasives.exit (1)
> 
> But this is clearly a hack.

i would use an execption :

exception Sould_never_be_here

let f () = while true do () done ; raise Sould_never_be_here

-- 
Rémi Vanicat
vanicat@labri.u-bordeaux.fr
http://dept-info.labri.u-bordeaux.fr/~vanicat

Re: bottom types and threaded exits

[Pierre Weis]

[...]
> Trying to define a type of int -> 'a naturally leads
> to a compiler error of 'a being unbound.

What about:

# let rec loop x = loop (x + 1);;
val loop : int -> 'a = <fun>

This is a pretty convincing non-terminating computation, isn't it ?

Pierre Weis

INRIA, Projet Cristal, Pierre.Weis@inria.fr, http://cristal.inria.fr/~weis/

bottom types and threaded exits

[Julian Assange]

Pervasives.exit is of type int -> 'a

Here we see ocaml using 'a to represent _|_. This hack is presumably
so type unification still works in the face of potentially
non-terminating computations, e.g:

let f a =
        try 
          f a
        with
          Failure _ -> exit(1)

How can one force 'a? For instance, Thread.exit and

        let f () = while true do () done 

has a type of unit -> unit.

One can write something such as

        let f () = while true do () done ; Pervasives.exit (1)

But this is clearly a hack.

If the type of Pervasices.exit is traced back, it originates in the
`external affairs powers' of the ocaml type system and is thus not
prone to type inferment. Functions never normally cause an *increase*
in generality. Trying to define a type of int -> 'a naturally leads
to a compiler error of 'a being unbound.

Cheers,
Julian.