Typing of infinite loops

9 replies

Tue, 2009-02-17, 15:58

Dave Griffith

Joined: 2009-01-14,

Playing around with edge cases and automated transformations of Scala code, I've found something strange. I would expect something like this

def foo():Int = {
 var x:Int = 0
     while(true){
       if(x > 3){
         return x;
       }
       x += 1
     }
}

to compile, but it doesn't. This is because while loops (and do loops) have type Unit, even when their conditions are constant true. To make it compile, I have to tag a line on the end like

  -1 //This can't happen

which is always a sign you are doing things wrong. Now this being Scala, the workaround is both easy and gorgeous. I just define my own control structure:

  def forever[A](body: => A):Nothing = {
    body
    forever(body)
  }

but it seems like it would be a pretty trivial (and non-breaking) change to have while(true){} and do{}while(true) type as Nothing, rather than Unit. It certainly fits imperative intuition better (to extent that such a thing is even a tertiary concern in Scala language design).
View this message in context: Typing of infinite loops
Sent from the Scala - User mailing list archive at Nabble.com.

Tue, 2009-02-17, 18:07

extempore

Joined: 2008-12-17,

Re: Typing of infinite loops

On Tue, Feb 17, 2009 at 06:57:10AM -0800, Dave Griffith wrote:
> but it seems like it would be a pretty trivial (and non-breaking) change to
> have while(true){} and do{}while(true) type as Nothing, rather than Unit.

This opens the door to a world of uncertainty. What is the type of this?

val x = true
while (x) { ... }

Or this?

while (5 == 5) { ... }

Lots more come to mind. The only way you have any chance of being mostly unsurprising is to only have the
literal "while(true)" type to Nothing (which could well be what you had in mind) and nothing else, but such a
special case is easily abstracted and special-casing the language requires compelling motivation.

I could perhaps see the merit of a def loop(body: => Unit): Nothing in Predef, but I think the inconvenience of
having to include a dummy value is pretty small. I fully agree it's aesthetically displeasing.

Tue, 2009-02-17, 18:37

DRMacIver

Joined: 2008-09-02,

Re: Typing of infinite loops

On Tue, Feb 17, 2009 at 4:35 PM, Paul Phillips <paulp@improving.org> wrote:

On Tue, Feb 17, 2009 at 06:57:10AM -0800, Dave Griffith wrote:
> but it seems like it would be a pretty trivial (and non-breaking) change to
> have while(true){} and do{}while(true) type as Nothing, rather than Unit.

This opens the door to a world of uncertainty. What is the type of this?

val x = true
while (x) { ... }

Or this?

while (5 == 5) { ... }

Lots more come to mind. The only way you have any chance of being mostly unsurprising is to only have the
literal "while(true)" type to Nothing (which could well be what you had in mind) and nothing else, but such a
special case is easily abstracted and special-casing the language requires compelling motivation.

Actually because of the way constant folding works in scalac, making this work for while(true) { ... } would cause it to work automatically for all the cases where you'd expect it to. But...

I could perhaps see the merit of a def loop(body: => Unit): Nothing in Predef, but I think the inconvenience of
having to include a dummy value is pretty small. I fully agree it's aesthetically displeasing.

A loop method in Predef (or something equivalent but differently named) seems much more appealing.

Tue, 2009-02-17, 19:47

extempore

Joined: 2008-12-17,

Re: Typing of infinite loops

On Tue, Feb 17, 2009 at 05:14:09PM +0000, David MacIver wrote:
> Actually because of the way constant folding works in scalac, making this
> work for while(true) { ... } would cause it to work automatically for all
> the cases where you'd expect it to.

For unspecified values of you? What about...

final def test() = true // or, why not lazy final val test = true
while (test()) { ... }

Or drawing on our old favorite, https://lampsvn.epfl.ch/trac/scala/ticket/1458...

object Bob { val test = true } // alternatively try final val test = true
while (Bob.test) { ... }

Maybe...

final val x = null
while (!x.isInstanceOf[String]) { ... } // guaranteed always true

I'm not sure what I expect all these to do, but I'm pretty sure I'd surprise myself eventually.

Tue, 2009-02-17, 22:57

Robert Fischer

Joined: 2009-01-31,

Re: Typing of infinite loops

In OCaml, it's a return value of "'a" which is OCaml's way of telling you that it has no idea what
the return value is, and you wouldn't be able to get at it/do anything with it anyway.

~~ Robert.

David MacIver wrote:
>
>
> On Tue, Feb 17, 2009 at 4:35 PM, Paul Phillips > wrote:
>
> On Tue, Feb 17, 2009 at 06:57:10AM -0800, Dave Griffith wrote:
> > but it seems like it would be a pretty trivial (and non-breaking)
> change to
> > have while(true){} and do{}while(true) type as Nothing, rather
> than Unit.
>
> This opens the door to a world of uncertainty. What is the type of
> this?
>
> val x = true
> while (x) { ... }
>
> Or this?
>
> while (5 == 5) { ... }
>
> Lots more come to mind. The only way you have any chance of being
> mostly unsurprising is to only have the
> literal "while(true)" type to Nothing (which could well be what you
> had in mind) and nothing else, but such a
> special case is easily abstracted and special-casing the language
> requires compelling motivation.
>
>
> Actually because of the way constant folding works in scalac, making
> this work for while(true) { ... } would cause it to work automatically
> for all the cases where you'd expect it to. But...
>
>
>
> I could perhaps see the merit of a def loop(body: => Unit): Nothing
> in Predef, but I think the inconvenience of
> having to include a dummy value is pretty small. I fully agree it's
> aesthetically displeasing.
>
>
> A loop method in Predef (or something equivalent but differently named)
> seems much more appealing.

Tue, 2009-02-17, 23:17

Christian Szegedy

Joined: 2009-02-08,

Re: Typing of infinite loops

I think it is hard to compare OCaml's type system with scala's since ocaml types do
not form a class hierarchy, still you may be right the Nothing is closes to return type
'a of Ocaml, simply because it can be unified with anything without changing the
result type.

However Ocaml types infinite loops as of type unit, as doing otherwise would open
the same can of worms:

# let f () = while true do () done;;
val f : unit -> unit = <fun>

On 2/17/09, Robert Fischer <robert.fischer@smokejumperit.com> wrote:

In OCaml, it's a return value of "'a" which is OCaml's way of telling you that it has no idea what the return value is, and you wouldn't be able to get at it/do anything with it anyway.

~~ Robert.

David MacIver wrote:

On Tue, Feb 17, 2009 at 4:35 PM, Paul Phillips <paulp@improving.org <mailto:paulp@improving.org>> wrote:

On Tue, Feb 17, 2009 at 06:57:10AM -0800, Dave Griffith wrote:
> but it seems like it would be a pretty trivial (and non-breaking)
change to
> have while(true){} and do{}while(true) type as Nothing, rather
than Unit.

This opens the door to a world of uncertainty. What is the type of
this?

val x = true
while (x) { ... }

Or this?

while (5 == 5) { ... }

Lots more come to mind. The only way you have any chance of being
mostly unsurprising is to only have the
literal "while(true)" type to Nothing (which could well be what you
had in mind) and nothing else, but such a
special case is easily abstracted and special-casing the language
requires compelling motivation.

Actually because of the way constant folding works in scalac, making this work for while(true) { ... } would cause it to work automatically for all the cases where you'd expect it to. But...

I could perhaps see the merit of a def loop(body: => Unit): Nothing
in Predef, but I think the inconvenience of
having to include a dummy value is pretty small. I fully agree it's
aesthetically displeasing.

A loop method in Predef (or something equivalent but differently named) seems much more appealing.

Tue, 2009-02-17, 23:27

Robert Fischer

Joined: 2009-01-31,

Re: Typing of infinite loops

True on both counts. I figured I'd throw that out there as a perspective. Although it probably
just confused things further, as I was confusing nonterminating functions (typed with unit) with
nonreturning functions (typed with 'a).

# let x = raise;;
val x : exn -> 'a =

~~ Robert.

Christian Szegedy wrote:
> I think it is hard to compare OCaml's type system with scala's since
> ocaml types do
> not form a class hierarchy, still you may be right the Nothing is closes
> to return type
> 'a of Ocaml, simply because it can be unified with anything without
> changing the
> result type.
>
> However Ocaml types infinite loops as of type unit, as doing otherwise
> would open
> the same can of worms:
>
> # let f () = while true do () done;;
> val f : unit -> unit =
>
>
> On 2/17/09, *Robert Fischer* > wrote:
>
> In OCaml, it's a return value of "'a" which is OCaml's way of
> telling you that it has no idea what the return value is, and you
> wouldn't be able to get at it/do anything with it anyway.
>
> ~~ Robert.
>
> David MacIver wrote:
>
>
>
> On Tue, Feb 17, 2009 at 4:35 PM, Paul Phillips
>
> >> wrote:
>
> On Tue, Feb 17, 2009 at 06:57:10AM -0800, Dave Griffith wrote:
> > but it seems like it would be a pretty trivial (and
> non-breaking)
> change to
> > have while(true){} and do{}while(true) type as Nothing, rather
> than Unit.
>
> This opens the door to a world of uncertainty. What is the
> type of
> this?
>
> val x = true
> while (x) { ... }
>
> Or this?
>
> while (5 == 5) { ... }
>
> Lots more come to mind. The only way you have any chance of
> being
> mostly unsurprising is to only have the
> literal "while(true)" type to Nothing (which could well be
> what you
> had in mind) and nothing else, but such a
> special case is easily abstracted and special-casing the language
> requires compelling motivation.
>
>
> Actually because of the way constant folding works in scalac,
> making this work for while(true) { ... } would cause it to work
> automatically for all the cases where you'd expect it to. But...
>
>
> I could perhaps see the merit of a def loop(body: => Unit):
> Nothing
> in Predef, but I think the inconvenience of
> having to include a dummy value is pretty small. I fully
> agree it's
> aesthetically displeasing.
>
>
> A loop method in Predef (or something equivalent but differently
> named) seems much more appealing.
>
>
> --
> ~~ Robert Fischer.
> Grails Training http://GroovyMag.com/training
> Smokejumper Consulting http://SmokejumperIT.com
> Enfranchised Mind Blog http://EnfranchisedMind.com/blog
>
> Check out my book, "Grails Persistence with GORM and GSQL"!
> http://www.smokejumperit.com/redirect.html
>
>

Tue, 2009-02-17, 23:37

Christian Szegedy

Joined: 2009-02-08,

Re: Typing of infinite loops

Some more additional examples for OCaml's typing:

# let f () = failwith "Error";;
val f : unit -> 'a = <fun>

However:

# let f() = if false then 1 else failwith "error";;
val f : unit -> int = <fun>

IMO this is the most logical typing and well aligned with what scala does:
The return type does not depend on reachability analysis of the program code,
but on pure syntax-based unification.

On 2/17/09, Christian Szegedy <christian.szegedy@gmail.com> wrote:

I think it is hard to compare OCaml's type system with scala's since ocaml types do
not form a class hierarchy, still you may be right the Nothing is closes to return type
'a of Ocaml, simply because it can be unified with anything without changing the
result type.

However Ocaml types infinite loops as of type unit, as doing otherwise would open
the same can of worms:

# let f () = while true do () done;;
val f : unit -> unit = <fun>

On 2/17/09, Robert Fischer <robert.fischer@smokejumperit.com> wrote:
In OCaml, it's a return value of "'a" which is OCaml's way of telling you that it has no idea what the return value is, and you wouldn't be able to get at it/do anything with it anyway.

~~ Robert.

David MacIver wrote:

On Tue, Feb 17, 2009 at 4:35 PM, Paul Phillips <paulp@improving.org <mailto:paulp@improving.org>> wrote:

On Tue, Feb 17, 2009 at 06:57:10AM -0800, Dave Griffith wrote:
> but it seems like it would be a pretty trivial (and non-breaking)
change to
> have while(true){} and do{}while(true) type as Nothing, rather
than Unit.

This opens the door to a world of uncertainty. What is the type of
this?

val x = true
while (x) { ... }

Or this?

while (5 == 5) { ... }

Lots more come to mind. The only way you have any chance of being
mostly unsurprising is to only have the
literal "while(true)" type to Nothing (which could well be what you
had in mind) and nothing else, but such a
special case is easily abstracted and special-casing the language
requires compelling motivation.

Actually because of the way constant folding works in scalac, making this work for while(true) { ... } would cause it to work automatically for all the cases where you'd expect it to. But...

I could perhaps see the merit of a def loop(body: => Unit): Nothing
in Predef, but I think the inconvenience of
having to include a dummy value is pretty small. I fully agree it's
aesthetically displeasing.

A loop method in Predef (or something equivalent but differently named) seems much more appealing.

Tue, 2009-02-17, 23:47

Robert Fischer

Joined: 2009-01-31,

Re: Typing of infinite loops

Yeah -- that's *why* it's 'a -- that way, the return value unifies with any other possible return
value. So any branch that reads "if x then y else failwith z" becomes typed the same as "y".

~~ Robert.

Christian Szegedy wrote:
> Some more additional examples for OCaml's typing:
>
> # let f () = failwith "Error";;
> val f : unit -> 'a =
>
> However:
>
> # let f() = if false then 1 else failwith "error";;
> val f : unit -> int =
>
> IMO this is the most logical typing and well aligned with what scala does:
> The return type does not depend on reachability analysis of the program
> code,
> but on pure syntax-based unification.
>
> On 2/17/09, *Christian Szegedy* > wrote:
>
> I think it is hard to compare OCaml's type system with scala's since
> ocaml types do
> not form a class hierarchy, still you may be right the Nothing is
> closes to return type
> 'a of Ocaml, simply because it can be unified with anything without
> changing the
> result type.
>
> However Ocaml types infinite loops as of type unit, as doing
> otherwise would open
> the same can of worms:
>
> # let f () = while true do () done;;
> val f : unit -> unit =
>
>
>
> On 2/17/09, *Robert Fischer* > wrote:
>
> In OCaml, it's a return value of "'a" which is OCaml's way of
> telling you that it has no idea what the return value is, and
> you wouldn't be able to get at it/do anything with it anyway.
>
> ~~ Robert.
>
> David MacIver wrote:
>
>
>
> On Tue, Feb 17, 2009 at 4:35 PM, Paul Phillips
>
> >>
> wrote:
>
> On Tue, Feb 17, 2009 at 06:57:10AM -0800, Dave Griffith
> wrote:
> > but it seems like it would be a pretty trivial (and
> non-breaking)
> change to
> > have while(true){} and do{}while(true) type as
> Nothing, rather
> than Unit.
>
> This opens the door to a world of uncertainty. What is
> the type of
> this?
>
> val x = true
> while (x) { ... }
>
> Or this?
>
> while (5 == 5) { ... }
>
> Lots more come to mind. The only way you have any chance
> of being
> mostly unsurprising is to only have the
> literal "while(true)" type to Nothing (which could well
> be what you
> had in mind) and nothing else, but such a
> special case is easily abstracted and special-casing the
> language
> requires compelling motivation.
>
>
> Actually because of the way constant folding works in
> scalac, making this work for while(true) { ... } would cause
> it to work automatically for all the cases where you'd
> expect it to. But...
>
>
> I could perhaps see the merit of a def loop(body: =>
> Unit): Nothing
> in Predef, but I think the inconvenience of
> having to include a dummy value is pretty small. I fully
> agree it's
> aesthetically displeasing.
>
>
> A loop method in Predef (or something equivalent but
> differently named) seems much more appealing.
>
>
> --
> ~~ Robert Fischer.
> Grails Training http://GroovyMag.com/training
> Smokejumper Consulting http://SmokejumperIT.com
> Enfranchised Mind Blog http://EnfranchisedMind.com/blog
>
> Check out my book, "Grails Persistence with GORM and GSQL"!
> http://www.smokejumperit.com/redirect.html
>
>
>

Tue, 2009-02-17, 23:57

Christian Szegedy

Joined: 2009-02-08,

Re: Typing of infinite loops

On 2/17/09, Dave Griffith <dave.l.griffith@gmail.com> wrote:

to compile, but it doesn't. This is because while loops (and do loops) have type Unit, even when their conditions are constant true. To make it compile, I have to tag a line on the end like
  -1 //This can't happen

I'd rather put instead :

error("Unreachable branch")

which both signifies and *checks* that the execution does not reach the designated spot.

Scala Main Menu

Typing of infinite loops

Scala Quick Links

Featured News

User login