This page is no longer maintained — Please continue to the home page at www.scala-lang.org

Improve type inference engine

28 replies
Antoras
Joined: 2010-05-23,
User offline. Last seen 1 year 19 weeks ago.

Scalas type inference engine is not as powerful than Haskells. See the
following code snippet:

size xs = loop xs 0
where
loop [] acc = acc
loop (_ : xs) acc = loop xs (acc+1)

In Scala one have to write:

def size[A](xs: List[A]) = {
def loop(xs: List[A], acc: Int): Int = xs match {
case Nil => acc
case _ :: xs => loop(xs, acc+1)
}
loop(xs, 0)
}

This is not possible:

def size(xs) = {
def loop(xs, acc) = xs match {
case Nil => acc
case _ :: xs => loop(xs, acc+1)
}
loop(xs, 0)
}

On StackOverflow I asked some months ago why this is not possible[1].
But now I want to know if it is possible to implement such a feature.
For example it may be possible to write:

def size[A](xs: List[A]) = {
local def loop(xs, acc) = xs match {
case Nil => acc
case _ :: xs => loop(xs, acc+1)
}
loop(xs, 0)
}

Whenever a keyword such as 'local' is used, the compiler can switch to
another type inference engine and correctly infer the types. Of course,
because of sub-typing this may be possible only in some scopes, in this
example only inside of a method.

What do you think/know about that? Is it possible to create such a "type
inference switch" in Scala or are there some technical barriers which
make this impossible?

[1]
http://stackoverflow.com/questions/7234095/why-is-scalas-type-inference-...

Simon Ochsenreither
Joined: 2011-07-17,
User offline. Last seen 42 years 45 weeks ago.
Re: Improve type inference engine
Hi,
 
Scalas type inference engine is not as powerful than Haskells.

Yes. And Scala is not Haskell, btw.

Sorry for my snarky remark, but considering that time and ressources are limited, there are quite some places where better inference would be more needed and which wouldn't require writing “another type inference engine” to implement it.

Imho this idea looks nice for some one-line snippets but fails to pull it weight in “real-world” code. Additionally, I don't like to have another keyword, e. g. yet-another-way-to-write-code.

Bye,

Simon
Antoras
Joined: 2010-05-23,
User offline. Last seen 1 year 19 weeks ago.
Re: Re: Improve type inference engine
Am 01.01.2012 23:55, schrieb Simon Ochsenreither:
Hi,
 
Scalas type inference engine is not as powerful than Haskells.

Yes. And Scala is not Haskell, btw.

Sorry for my snarky remark, but considering that time and ressources are limited, there are quite some places where better inference would be more needed and which wouldn't require writing “another type inference engine” to implement it.
This was more a theoretical question. I want to know if it is technically possible and not if there are people who can realize it. This would be part of further questions...


Imho this idea looks nice for some one-line snippets but fails to pull it weight in “real-world” code.
Why? In Haskell it works fine thus there can be a way to realize it in Scala.

Additionally, I don't like to have another keyword, e. g. yet-another-way-to-write-code.
Ok, that is a point. But maybe it is possible to realize this without the use of a new keyword.
H-star Development
Joined: 2010-04-14,
User offline. Last seen 2 years 26 weeks ago.
Re: Re: Improve type inference engine

the "total" type inference could be automatically switched on for all private/local methods where a single type fits.

however, i don't think it's a good idea to completely trim all type declarations out of the code. at least not until every ide has a "insert/remove all type annotations" switch in case i forgot what a variables type was and need to quickly show it.

type inference can add to the reading time what it cuts off the writing time if the type is hidden behind 5 other calls.

-------- Original-Nachricht --------
> Datum: Mon, 02 Jan 2012 14:07:56 +0100
> Von: Antoras
> An: scala-debate [at] googlegroups [dot] com
> Betreff: Re: [scala-debate] Re: Improve type inference engine

> Am 01.01.2012 23:55, schrieb Simon Ochsenreither:
> > Hi,
> >
> > Scalas type inference engine is not as powerful than Haskells.
> >
> >
> > Yes. And Scala is not Haskell, btw.
> >
> > Sorry for my snarky remark, but considering that time and ressources
> > are limited, there are quite some places where better inference would
> > be more needed and which wouldn't require writing “another type
> > inference engine” to implement it.
> This was more a theoretical question. I want to know if it is
> technically possible and not if there are people who can realize it.
> This would be part of further questions...
>
> >
> > Imho this idea looks nice for some one-line snippets but fails to pull
> > it weight in “real-world” code.
> Why? In Haskell it works fine thus there can be a way to realize it in
> Scala.
>
> > Additionally, I don't like to have another keyword, e. g.
> > yet-another-way-to-write-code.
> Ok, that is a point. But maybe it is possible to realize this without
> the use of a new keyword.

moors
Joined: 2010-10-06,
User offline. Last seen 36 weeks 4 days ago.
Re: Re: Improve type inference engine
Why? In Haskell it works fine thus there can be a way to realize it in Scala.
not really, Haskell does not have subtyping, for one, and they don't mind whole-program compilation (instead of separate compilation in Scala/Java/most OO languages)
we will never infer (public) signatures, as that's about as hard/"unreasonable" as inferring documentation(which type the programmer choses in the subtyping hierarchy is a form of documentation! as a simple example: did you pick Iterable[T] or List[T] as the return-type of some method?)
that said...
for private methods, such as `loop` in your example, I think it would be possible -- and maybe even desirable -- to infer types,but it would be pretty hard to spec and implement, with relatively little gain (that's why we haven't done it)

cheersadriaan
dcsobral
Joined: 2009-04-23,
User offline. Last seen 38 weeks 5 days ago.
Re: Re: Improve type inference engine

On Tue, Jan 3, 2012 at 11:40, Adriaan Moors wrote:
>> Why? In Haskell it works fine thus there can be a way to realize it in
>> Scala.
>
> not really, Haskell does not have subtyping, for one, and they don't mind
> whole-program compilation (instead of separate compilation in
> Scala/Java/most OO languages)
>
> we will never infer (public) signatures, as that's about as
> hard/"unreasonable" as inferring documentation
> (which type the programmer choses in the subtyping hierarchy is a form of
> documentation!
>  as a simple example: did you pick Iterable[T] or List[T] as the return-type
> of some method?)
>
> that said...
>
> for private methods, such as `loop` in your example, I think it would be
> possible -- and maybe even desirable -- to infer types,
> but it would be pretty hard to spec and implement, with relatively little
> gain (that's why we haven't done it)

I have proposed something like this just these days -- on twitter, I
think. I'm wondering about this particular case:

def f = {
def g(x, y) = x * y
g(3, 2)
}

The restriction is that g cannot be used in eta expansion without
having its type declared. Given this restriction, then the types for
its parameters can be inferred just like a val. Some complications
are:

def fat(n: Int) = {
def g(x, y): Int = if (x == 1) y else g(x - 1, x * y) // recursion
g(n, 1)
}

def f = {
def g(x, y) = x * y
g(3, 2) * g (5.0, 2.1) // multiple call sites
}

Multiple call sites would require unification, so I'm guessing this is
much on par with return statements -- they make it too hard to infer
the return type, so it might be better to disallow it. The type could
be inferred from the first call, marked somehow, and then an error
message be generated if a second call is found. More leniently, such
error could be produced only if a call with types that don't match
what has been inferred don't match.

Recursion seems more difficult (to me), but, on the other hand, it is
the case that I most would like to be handled: I hate the repetitive
typing whenever I write an inner function to implement a tail
recursion for the method.

If typing the whole inner function could be deferred until a call site
is found, then the parameters could be inferred from the call site,
and the rest would follow.

Does that look sound to you?

H-star Development
Joined: 2010-04-14,
User offline. Last seen 2 years 26 weeks ago.
Re: Re: Improve type inference engine

if here is just one usage (or several, but all are equal in the types they accept), there already is an algorithm:

list.filter(_.iWantThat)

it should be relatively easy to just use that algorithm at these special cases.

for the return type inference: what exactly is the problem? if you just ignore the recursive call, isn't that enough for 80%+ of all cases?

def fak(n:Int) = if ( n == 0) 1 else n*fak(n-1)

eliminate "fak(n-1)" and that just leaves 1 which means there will be an Int returned.

-------- Original-Nachricht --------
> Datum: Tue, 3 Jan 2012 12:01:53 -0200
> Von: Daniel Sobral
> An: scala-debate [at] googlegroups [dot] com
> Betreff: Re: [scala-debate] Re: Improve type inference engine

> On Tue, Jan 3, 2012 at 11:40, Adriaan Moors
> wrote:
> >> Why? In Haskell it works fine thus there can be a way to realize it in
> >> Scala.
> >
> > not really, Haskell does not have subtyping, for one, and they don't
> mind
> > whole-program compilation (instead of separate compilation in
> > Scala/Java/most OO languages)
> >
> > we will never infer (public) signatures, as that's about as
> > hard/"unreasonable" as inferring documentation
> > (which type the programmer choses in the subtyping hierarchy is a form
> of
> > documentation!
> >  as a simple example: did you pick Iterable[T] or List[T] as the
> return-type
> > of some method?)
> >
> > that said...
> >
> > for private methods, such as `loop` in your example, I think it would be
> > possible -- and maybe even desirable -- to infer types,
> > but it would be pretty hard to spec and implement, with relatively
> little
> > gain (that's why we haven't done it)
>
> I have proposed something like this just these days -- on twitter, I
> think. I'm wondering about this particular case:
>
> def f = {
> def g(x, y) = x * y
> g(3, 2)
> }
>
> The restriction is that g cannot be used in eta expansion without
> having its type declared. Given this restriction, then the types for
> its parameters can be inferred just like a val. Some complications
> are:
>
> def fat(n: Int) = {
> def g(x, y): Int = if (x == 1) y else g(x - 1, x * y) // recursion
> g(n, 1)
> }
>
> def f = {
> def g(x, y) = x * y
> g(3, 2) * g (5.0, 2.1) // multiple call sites
> }
>
> Multiple call sites would require unification, so I'm guessing this is
> much on par with return statements -- they make it too hard to infer
> the return type, so it might be better to disallow it. The type could
> be inferred from the first call, marked somehow, and then an error
> message be generated if a second call is found. More leniently, such
> error could be produced only if a call with types that don't match
> what has been inferred don't match.
>
> Recursion seems more difficult (to me), but, on the other hand, it is
> the case that I most would like to be handled: I hate the repetitive
> typing whenever I write an inner function to implement a tail
> recursion for the method.
>
> If typing the whole inner function could be deferred until a call site
> is found, then the parameters could be inferred from the call site,
> and the rest would follow.
>
> Does that look sound to you?
>

dcsobral
Joined: 2009-04-23,
User offline. Last seen 38 weeks 5 days ago.
Re: Re: Improve type inference engine

On Tue, Jan 3, 2012 at 12:18, Dennis Haupt wrote:
> if here is just one usage (or several, but all are equal in the types they accept), there already is an algorithm:
>
> list.filter(_.iWantThat)

That assumes the compiler has typed everything else, and is now going
back to type these things. In other words, typing would need to be
applied multiple times, until no more types can be inferred. I'm
guessing it would be slower and more complex than what exists, but I'm
pretty sure it is *not* what exists. What exists is that types are
inferred left to right, top to bottom, without backtracking.

>
> it should be relatively easy to just use that algorithm at these special cases.
>
> for the return type inference: what exactly is the problem? if you just ignore the recursive call, isn't that enough for 80%+ of all cases?
>
> def fak(n:Int) = if ( n == 0) 1 else n*fak(n-1)
>
> eliminate "fak(n-1)" and that just leaves 1 which means there will be an Int returned.

That's what you, human, seeing the whole line for what it is, is
doing. What Scala is doing is more like this:

def fak(n: Int) = E -- mmm, no type given, I need to infer it from expression E

if C E1 else E2 -- an if statement; I need to unify E1 and E2

H-star Development
Joined: 2010-04-14,
User offline. Last seen 2 years 26 weeks ago.
Re: Re: Improve type inference engine

-------- Original-Nachricht --------
> Datum: Tue, 3 Jan 2012 13:37:47 -0200
> Von: Daniel Sobral
> An: Dennis Haupt
> CC: scala-debate [at] googlegroups [dot] com
> Betreff: Re: [scala-debate] Re: Improve type inference engine

> On Tue, Jan 3, 2012 at 12:18, Dennis Haupt wrote:
> > if here is just one usage (or several, but all are equal in the types
> they accept), there already is an algorithm:
> >
> > list.filter(_.iWantThat)
>
> That assumes the compiler has typed everything else, and is now going
> back to type these things. In other words, typing would need to be
> applied multiple times, until no more types can be inferred. I'm
> guessing it would be slower and more complex than what exists, but I'm
> pretty sure it is *not* what exists. What exists is that types are
> inferred left to right, top to bottom, without backtracking.
>
> >
> > it should be relatively easy to just use that algorithm at these special
> cases.
> >
> > for the return type inference: what exactly is the problem? if you just
> ignore the recursive call, isn't that enough for 80%+ of all cases?
> >
> > def fak(n:Int) = if ( n == 0) 1 else n*fak(n-1)
> >
> > eliminate "fak(n-1)" and that just leaves 1 which means there will be an
> Int returned.
>
> That's what you, human, seeing the whole line for what it is, is
> doing. What Scala is doing is more like this:
>
> def fak(n: Int) = E -- mmm, no type given, I need to infer it from
> expression E
>
> if C E1 else E2 -- an if statement; I need to unify E1 and E2
>
> 1 -- ok this is an Int
>
> Int.*(E3) -- I need to type E3 to find out what's the type of this
> expression
>
> fak(E4) -- I need to type E4 to see what is being done here
>
> Int.-(Int) -- This returns Int
>
> fak(Int) -- Ok, I see this method, but what is its return type?

i don't see the problem. at this step, you see thar fak(Int) is recursive and should be ignored which just leaves Int as a return type.

>
> At which point it is a bit hard to do something about it. If it was a
> *tail* recursion, it would be a _bit_ easier. The compiler could,
> theoretically, return E2 as something meaning "mirror any type bounds
> on unification", and complain if that's the type inferred for the
> return value of the method. In your example, however, it still needs
> to type E2, and to do that it needs to type E3, which requires typing
> fak, which requires typing E2. If you exclude E3 from being typed
> because it is being recursed, it cannot determine what "*" method is
> being called, and, therefore, what result must be unified with E1.
>
> >
> > -------- Original-Nachricht --------
> >> Datum: Tue, 3 Jan 2012 12:01:53 -0200
> >> Von: Daniel Sobral
> >> An: scala-debate [at] googlegroups [dot] com
> >> Betreff: Re: [scala-debate] Re: Improve type inference engine
> >
> >> On Tue, Jan 3, 2012 at 11:40, Adriaan Moors
> >> wrote:
> >> >> Why? In Haskell it works fine thus there can be a way to realize it
> in
> >> >> Scala.
> >> >
> >> > not really, Haskell does not have subtyping, for one, and they don't
> >> mind
> >> > whole-program compilation (instead of separate compilation in
> >> > Scala/Java/most OO languages)
> >> >
> >> > we will never infer (public) signatures, as that's about as
> >> > hard/"unreasonable" as inferring documentation
> >> > (which type the programmer choses in the subtyping hierarchy is a
> form
> >> of
> >> > documentation!
> >> >  as a simple example: did you pick Iterable[T] or List[T] as the
> >> return-type
> >> > of some method?)
> >> >
> >> > that said...
> >> >
> >> > for private methods, such as `loop` in your example, I think it would
> be
> >> > possible -- and maybe even desirable -- to infer types,
> >> > but it would be pretty hard to spec and implement, with relatively
> >> little
> >> > gain (that's why we haven't done it)
> >>
> >> I have proposed something like this just these days -- on twitter, I
> >> think. I'm wondering about this particular case:
> >>
> >> def f = {
> >>   def g(x, y) = x * y
> >>   g(3, 2)
> >> }
> >>
> >> The restriction is that g cannot be used in eta expansion without
> >> having its type declared. Given this restriction, then the types for
> >> its parameters can be inferred just like a val. Some complications
> >> are:
> >>
> >> def fat(n: Int) = {
> >>   def g(x, y): Int = if (x == 1) y else g(x - 1, x * y) // recursion
> >>   g(n, 1)
> >> }
> >>
> >> def f = {
> >>   def g(x, y) = x * y
> >>   g(3, 2) * g (5.0, 2.1)  // multiple call sites
> >> }
> >>
> >> Multiple call sites would require unification, so I'm guessing this is
> >> much on par with return statements -- they make it too hard to infer
> >> the return type, so it might be better to disallow it. The type could
> >> be inferred from the first call, marked somehow, and then an error
> >> message be generated if a second call is found. More leniently, such
> >> error could be produced only if a call with types that don't match
> >> what has been inferred don't match.
> >>
> >> Recursion seems more difficult (to me), but, on the other hand, it is
> >> the case that I most would like to be handled: I hate the repetitive
> >> typing whenever I write an inner function to implement a tail
> >> recursion for the method.
> >>
> >> If typing the whole inner function could be deferred until a call site
> >> is found, then the parameters could be inferred from the call site,
> >> and the rest would follow.
> >>
> >> Does that look sound to you?
> >>
> >> --
> >> Daniel C. Sobral
> >>
> >> I travel to the future all the time.
>
>
>

Lars Hupel
Joined: 2010-06-23,
User offline. Last seen 44 weeks 3 days ago.
Re: Improve type inference engine

> i don't see the problem. at this step, you see thar fak(Int) is
> recursive and should be ignored which just leaves Int as a return
> type.

You can't "just" ignore recursive calls during type inference. Consider
this one:

def f(n: Int) = f(n + 1)

What is the return type? `Nothing`?

Or:

def f[A](list: List[A]) = f(List(list))

`Nothing`? Or `List[Nothing]`? Or `List[List[Any]]`?

H-star Development
Joined: 2010-04-14,
User offline. Last seen 2 years 26 weeks ago.
Re: Re: Improve type inference engine

Am 03.01.2012 17:57, schrieb Lars Hupel:
>> i don't see the problem. at this step, you see thar fak(Int) is
>> recursive and should be ignored which just leaves Int as a return
>> type.
> You can't "just" ignore recursive calls during type inference.

yes i can. there just *has* to be something else that is returned,
because otherwise, nothing can ever be returned.

> Consider
> this one:
>
> def f(n: Int) = f(n + 1)
would not compile. and i don't see a problem with that. it would just
throw a stackoverflowerror anyway.

>
> What is the return type? `Nothing`?
>
> Or:
>
> def f[A](list: List[A]) = f(List(list))

stackoverflow again
>
> `Nothing`? Or `List[Nothing]`? Or `List[List[Any]]`?
>
>

if you want to prove me wrong, make up an example that does work in the
real world and where my algorithm fails.

H-star Development
Joined: 2010-04-14,
User offline. Last seen 2 years 26 weeks ago.
Re: Re: Improve type inference engine

Am 03.01.2012 16:37, schrieb Daniel Sobral:
> On Tue, Jan 3, 2012 at 12:18, Dennis Haupt wrote:
>> if here is just one usage (or several, but all are equal in the types they accept), there already is an algorithm:
>>
>> list.filter(_.iWantThat)
> That assumes the compiler has typed everything else, and is now going
> back to type these things.
i was thinking the other way round. if the compiler finds an untyped
function, it looks ahead at the usages. if there is only one, it applies
a little transformation to inline the function. then you have to code
above and your problem is gone, because in the code above, everything
works fine.

> In other words, typing would need to be
> applied multiple times, until no more types can be inferred. I'm
> guessing it would be slower and more complex than what exists, but I'm
> pretty sure it is *not* what exists. What exists is that types are
> inferred left to right, top to bottom, without backtracking.
>
>> it should be relatively easy to just use that algorithm at these special cases.
>>
>> for the return type inference: what exactly is the problem? if you just ignore the recursive call, isn't that enough for 80%+ of all cases?
>>
>> def fak(n:Int) = if ( n == 0) 1 else n*fak(n-1)
>>
>> eliminate "fak(n-1)" and that just leaves 1 which means there will be an Int returned.
> That's what you, human, seeing the whole line for what it is, is
> doing. What Scala is doing is more like this:
>
> def fak(n: Int) = E -- mmm, no type given, I need to infer it from expression E
>
> if C E1 else E2 -- an if statement; I need to unify E1 and E2
>
> 1 -- ok this is an Int
>
> Int.*(E3) -- I need to type E3 to find out what's the type of this expression
>
> fak(E4) -- I need to type E4 to see what is being done here
>
> Int.-(Int) -- This returns Int
>
> fak(Int) -- Ok, I see this method, but what is its return type?
>
> At which point it is a bit hard to do something about it. If it was a
> *tail* recursion, it would be a _bit_ easier. The compiler could,
> theoretically, return E2 as something meaning "mirror any type bounds
> on unification", and complain if that's the type inferred for the
> return value of the method. In your example, however, it still needs
> to type E2, and to do that it needs to type E3, which requires typing
> fak, which requires typing E2. If you exclude E3 from being typed
> because it is being recursed, it cannot determine what "*" method is
> being called, and, therefore, what result must be unified with E1.
>
>> -------- Original-Nachricht --------
>>> Datum: Tue, 3 Jan 2012 12:01:53 -0200
>>> Von: Daniel Sobral
>>> An: scala-debate [at] googlegroups [dot] com
>>> Betreff: Re: [scala-debate] Re: Improve type inference engine
>>> On Tue, Jan 3, 2012 at 11:40, Adriaan Moors
>>> wrote:
>>>>> Why? In Haskell it works fine thus there can be a way to realize it in
>>>>> Scala.
>>>> not really, Haskell does not have subtyping, for one, and they don't
>>> mind
>>>> whole-program compilation (instead of separate compilation in
>>>> Scala/Java/most OO languages)
>>>>
>>>> we will never infer (public) signatures, as that's about as
>>>> hard/"unreasonable" as inferring documentation
>>>> (which type the programmer choses in the subtyping hierarchy is a form
>>> of
>>>> documentation!
>>>> as a simple example: did you pick Iterable[T] or List[T] as the
>>> return-type
>>>> of some method?)
>>>>
>>>> that said...
>>>>
>>>> for private methods, such as `loop` in your example, I think it would be
>>>> possible -- and maybe even desirable -- to infer types,
>>>> but it would be pretty hard to spec and implement, with relatively
>>> little
>>>> gain (that's why we haven't done it)
>>> I have proposed something like this just these days -- on twitter, I
>>> think. I'm wondering about this particular case:
>>>
>>> def f = {
>>> def g(x, y) = x * y
>>> g(3, 2)
>>> }
>>>
>>> The restriction is that g cannot be used in eta expansion without
>>> having its type declared. Given this restriction, then the types for
>>> its parameters can be inferred just like a val. Some complications
>>> are:
>>>
>>> def fat(n: Int) = {
>>> def g(x, y): Int = if (x == 1) y else g(x - 1, x * y) // recursion
>>> g(n, 1)
>>> }
>>>
>>> def f = {
>>> def g(x, y) = x * y
>>> g(3, 2) * g (5.0, 2.1) // multiple call sites
>>> }
>>>
>>> Multiple call sites would require unification, so I'm guessing this is
>>> much on par with return statements -- they make it too hard to infer
>>> the return type, so it might be better to disallow it. The type could
>>> be inferred from the first call, marked somehow, and then an error
>>> message be generated if a second call is found. More leniently, such
>>> error could be produced only if a call with types that don't match
>>> what has been inferred don't match.
>>>
>>> Recursion seems more difficult (to me), but, on the other hand, it is
>>> the case that I most would like to be handled: I hate the repetitive
>>> typing whenever I write an inner function to implement a tail
>>> recursion for the method.
>>>
>>> If typing the whole inner function could be deferred until a call site
>>> is found, then the parameters could be inferred from the call site,
>>> and the rest would follow.
>>>
>>> Does that look sound to you?
>>>
>>> --
>>> Daniel C. Sobral
>>>
>>> I travel to the future all the time.
>
>

Alec Zorab
Joined: 2010-05-18,
User offline. Last seen 42 years 45 weeks ago.
Re: Re: Improve type inference engine

...snip...

if C E1 else E2 -- an if statement; I need to unify E1 and E2

H-star Development
Joined: 2010-04-14,
User offline. Last seen 2 years 26 weeks ago.
Re: Re: Improve type inference engine

exactly what i said :) except that i don't see a flaw

Am 03.01.2012 18:17, schrieb Alec Zorab:
> ...snip...
>
> if C E1 else E2 -- an if statement; I need to unify E1 and E2
>
> 1 -- ok this is an Int
>
> Int.*(E3) -- I need to type E3 to find out what's the type of this expression
>
> fak(E4) -- I need to type E4 to see what is being done here
>
> Int.-(Int) -- This returns Int
>
> fak(Int) -- Ok, I see this method, but what is its return type?
>
> ...snip...
>
> Can't you (in the general case) construct a list of all the returned
> types and then take the unifying type of all the types in that list?
> If you do that and treat recursive calls as not returning a type at
> all, then we get a train of thought like this:
>
> if C E1 else E2 -- an if statement; I need to unify E1 and E2
>
> 1 -- ok this is an Int, so my returned types for far look like Int :: Nil
>
> Int.*(E3) -- I need to type E3 to find out what's the type of this expression
>
> fak(E4) -- I need to type E4 to see what is being done here
>
> Int.-(Int) -- This returns Int
>
> fak(Int) -- Ok, I see this is a recursion, so this doesn't count., my
> returned types are still Int :: Nil
>
> Then when you end up with there being no terminating cases (eg def
> f(n: Int) = f(n + 1)) then you can just flag it as being an error.
>
> I imagine this has some massive flaw somewhere, but it's not
> immediately obvious to me what it is.
>

Stefan Zeiger
Joined: 2008-12-21,
User offline. Last seen 27 weeks 3 days ago.
Re: Re: Improve type inference engine

On 2012-01-03 17:57, Lars Hupel wrote:
> You can't "just" ignore recursive calls during type inference. Consider
> this one:
>
> def f(n: Int) = f(n + 1)
>
> What is the return type? `Nothing`?
>
> Or:
>
> def f[A](list: List[A]) = f(List(list))
>
> `Nothing`? Or `List[Nothing]`? Or `List[List[Any]]`?

If there is no non-recursive non-strict return path, you can always
infer Nothing. Without a base case for the recursion, it cannot
terminate normally. Things get more interesting if you add laziness into
the mix:

def f[T](x: => T): Option[T] = None

def g(x: Int) = f(g(x))

-sz

Lars Hupel
Joined: 2010-06-23,
User offline. Last seen 44 weeks 3 days ago.
Re: Improve type inference engine

Before getting into counterexamples, we have to make sure we are talking
about the same thing.

First I'd say we are talking about methods without type parameters. The
presence of type parameters couldn't be inferred anyway, I guess.

Next we assume that we have a single call site. Multiple, perhaps nested
call sites, would be additional fun.

So, essentially, it boils down to the question why the Scala compiler
doesn't infer the return type of recursive methods.

Back to an example.

// (I don't doubt that the type of the parameter can be inferred in
// these cases)
def f(x /* : A */) = if (cond(x)) z else f(rec(x))

(where the return type of `rec` is known)

My understanding of Scala's type inference is fairly limited, so my
naive try to translate your algorithm would be to solve

T = lub(typeof(z), T)

where `T` is the return type of `f` by setting `T` to `typeof(z)`. This
requires that `z` has a known type.

Is that correct?

If so, how would you solve that in a mutually recursive case?

If you wouldn't solve that at all, I don't see why it would be
beneficial to introduce your proposed solution.

Long story short: I admit that my example with non-termination isn't
relevant to this problem, and I agree that your idea can discover more
types, but I am doubtful whether this is general enough to make it worth
implementing.

Lars Hupel
Joined: 2010-06-23,
User offline. Last seen 44 weeks 3 days ago.
Re: Improve type inference engine

> If there is no non-recursive non-strict return path, you can always
> infer Nothing. Without a base case for the recursion, it cannot
> terminate normally.

Yeah that's true, my mistake.

> Things get more interesting if you add laziness into the mix:
>
> def f[T](x: => T): Option[T] = None
>
> def g(x: Int) = f(g(x))

A similar example without by-name parameters:

def f[T](x: T): Option[T] = None

def g(x: Int) = if (false) f(g(x)) else f(x)

Not sure what you want to demonstrate with that. Reduction to the
halting problem?

H-star Development
Joined: 2010-04-14,
User offline. Last seen 2 years 26 weeks ago.
Re: Re: Improve type inference engine

Am 03.01.2012 18:53, schrieb Lars Hupel:
> Before getting into counterexamples, we have to make sure we are talking
> about the same thing.
>
> First I'd say we are talking about methods without type parameters. The
> presence of type parameters couldn't be inferred anyway, I guess.
>
> Next we assume that we have a single call site. Multiple, perhaps nested
> call sites, would be additional fun.
it shouldn't matter
>
> So, essentially, it boils down to the question why the Scala compiler
> doesn't infer the return type of recursive methods.
>
> Back to an example.
>
> // (I don't doubt that the type of the parameter can be inferred in
> // these cases)
> def f(x /* : A */) = if (cond(x)) z else f(rec(x))
>
> (where the return type of `rec` is known)
>
> My understanding of Scala's type inference is fairly limited, so my
> naive try to translate your algorithm would be to solve
>
> T = lub(typeof(z), T)
>
> where `T` is the return type of `f` by setting `T` to `typeof(z)`. This
> requires that `z` has a known type.
>
> Is that correct?

yes
>
> If so, how would you solve that in a mutually recursive case?

you mean:

def x(i:Int) = if (i == 1000) foo else y(i-1)
def y(i:Int) = if (i == 1111) bar else x(i+2)

at first, you need to know that these methods are calling each other.
the compiler can do this because it complains if i don't specify a
return type, so i'll assume it can identify recursive methods.

my algorithm says:

def x = foo.class & *go deeper*
def y = bar.class & *recursion found, ignore* -> bar for now

up to x again:

return type is common superclass of foo.class & bar.class.

then go to y and infer its type - this time for real:

type of y = bar.class & type of x which is now known

you can still infer the types of the methods one after another.

>
> If you wouldn't solve that at all, I don't see why it would be
> beneficial to introduce your proposed solution.
>
> Long story short: I admit that my example with non-termination isn't
> relevant to this problem, and I agree that your idea can discover more
> types, but I am doubtful whether this is general enough to make it worth
> implementing.
>
>

dcsobral
Joined: 2009-04-23,
User offline. Last seen 38 weeks 5 days ago.
Re: Re: Improve type inference engine

On Tue, Jan 3, 2012 at 13:49, Dennis Haupt wrote:
>
>
> -------- Original-Nachricht --------
>> Datum: Tue, 3 Jan 2012 13:37:47 -0200
>> Von: Daniel Sobral
>> An: Dennis Haupt
>> CC: scala-debate [at] googlegroups [dot] com
>> Betreff: Re: [scala-debate] Re: Improve type inference engine
>
>> On Tue, Jan 3, 2012 at 12:18, Dennis Haupt wrote:
>> > if here is just one usage (or several, but all are equal in the types
>> they accept), there already is an algorithm:
>> >
>> > list.filter(_.iWantThat)
>>
>> That assumes the compiler has typed everything else, and is now going
>> back to type these things. In other words, typing would need to be
>> applied multiple times, until no more types can be inferred. I'm
>> guessing it would be slower and more complex than what exists, but I'm
>> pretty sure it is *not* what exists. What exists is that types are
>> inferred left to right, top to bottom, without backtracking.
>>
>> >
>> > it should be relatively easy to just use that algorithm at these special
>> cases.
>> >
>> > for the return type inference: what exactly is the problem? if you just
>> ignore the recursive call, isn't that enough for 80%+ of all cases?
>> >
>> > def fak(n:Int) = if ( n == 0) 1 else n*fak(n-1)
>> >
>> > eliminate "fak(n-1)" and that just leaves 1 which means there will be an
>> Int returned.
>>
>> That's what you, human, seeing the whole line for what it is, is
>> doing. What Scala is doing is more like this:
>>
>> def fak(n: Int) = E  -- mmm, no type given, I need to infer it from
>> expression E
>>
>> if C E1 else E2 -- an if statement; I need to unify E1 and E2
>>
>> 1 -- ok this is an Int
>>
>> Int.*(E3) -- I need to type E3 to find out what's the type of this
>> expression
>>
>> fak(E4) -- I need to type E4 to see what is being done here
>>
>> Int.-(Int) -- This returns Int
>>
>> fak(Int) -- Ok, I see this method, but what is its return type?
>
> i don't see the problem. at this step, you see thar fak(Int) is recursive and should be ignored which just leaves Int as a return type.

So let's make a problem:

def fak(n:Int) = if ( n == 0) 1 else n * fak(n-1) * 1.0

Oh, look, the return type wasn't Int after all! It was Double the whole time!

>
>>
>> At which point it is a bit hard to do something about it. If it was a
>> *tail* recursion, it would be a _bit_ easier. The compiler could,
>> theoretically, return E2 as something meaning "mirror any type bounds
>> on unification", and complain if that's the type inferred for the
>> return value of the method. In your example, however, it still needs
>> to type E2, and to do that it needs to type E3, which requires typing
>> fak, which requires typing E2. If you exclude E3 from being typed
>> because it is being recursed, it cannot determine what "*" method is
>> being called, and, therefore, what result must be unified with E1.
>>
>> >
>> > -------- Original-Nachricht --------
>> >> Datum: Tue, 3 Jan 2012 12:01:53 -0200
>> >> Von: Daniel Sobral
>> >> An: scala-debate [at] googlegroups [dot] com
>> >> Betreff: Re: [scala-debate] Re: Improve type inference engine
>> >
>> >> On Tue, Jan 3, 2012 at 11:40, Adriaan Moors
>> >> wrote:
>> >> >> Why? In Haskell it works fine thus there can be a way to realize it
>> in
>> >> >> Scala.
>> >> >
>> >> > not really, Haskell does not have subtyping, for one, and they don't
>> >> mind
>> >> > whole-program compilation (instead of separate compilation in
>> >> > Scala/Java/most OO languages)
>> >> >
>> >> > we will never infer (public) signatures, as that's about as
>> >> > hard/"unreasonable" as inferring documentation
>> >> > (which type the programmer choses in the subtyping hierarchy is a
>> form
>> >> of
>> >> > documentation!
>> >> >  as a simple example: did you pick Iterable[T] or List[T] as the
>> >> return-type
>> >> > of some method?)
>> >> >
>> >> > that said...
>> >> >
>> >> > for private methods, such as `loop` in your example, I think it would
>> be
>> >> > possible -- and maybe even desirable -- to infer types,
>> >> > but it would be pretty hard to spec and implement, with relatively
>> >> little
>> >> > gain (that's why we haven't done it)
>> >>
>> >> I have proposed something like this just these days -- on twitter, I
>> >> think. I'm wondering about this particular case:
>> >>
>> >> def f = {
>> >>   def g(x, y) = x * y
>> >>   g(3, 2)
>> >> }
>> >>
>> >> The restriction is that g cannot be used in eta expansion without
>> >> having its type declared. Given this restriction, then the types for
>> >> its parameters can be inferred just like a val. Some complications
>> >> are:
>> >>
>> >> def fat(n: Int) = {
>> >>   def g(x, y): Int = if (x == 1) y else g(x - 1, x * y) // recursion
>> >>   g(n, 1)
>> >> }
>> >>
>> >> def f = {
>> >>   def g(x, y) = x * y
>> >>   g(3, 2) * g (5.0, 2.1)  // multiple call sites
>> >> }
>> >>
>> >> Multiple call sites would require unification, so I'm guessing this is
>> >> much on par with return statements -- they make it too hard to infer
>> >> the return type, so it might be better to disallow it. The type could
>> >> be inferred from the first call, marked somehow, and then an error
>> >> message be generated if a second call is found. More leniently, such
>> >> error could be produced only if a call with types that don't match
>> >> what has been inferred don't match.
>> >>
>> >> Recursion seems more difficult (to me), but, on the other hand, it is
>> >> the case that I most would like to be handled: I hate the repetitive
>> >> typing whenever I write an inner function to implement a tail
>> >> recursion for the method.
>> >>
>> >> If typing the whole inner function could be deferred until a call site
>> >> is found, then the parameters could be inferred from the call site,
>> >> and the rest would follow.
>> >>
>> >> Does that look sound to you?
>> >>
>> >> --
>> >> Daniel C. Sobral
>> >>
>> >> I travel to the future all the time.
>>
>>
>>
>> --
>> Daniel C. Sobral
>>
>> I travel to the future all the time.

H-star Development
Joined: 2010-04-14,
User offline. Last seen 2 years 26 weeks ago.
Re: Re: Improve type inference engine

So let's make a problem: def fak(n:Int) = if ( n == 0) 1 else n *
fak(n-1) * 1.0 Oh, look, the return type wasn't Int after all! It was
Double the whole time!
>>
def fak(i:Int) = if (..) Int else Int * ignore * double

gives a double :)

Matthew Pocock 3
Joined: 2010-07-30,
User offline. Last seen 42 years 45 weeks ago.
Re: Re: Improve type inference engine


On 3 January 2012 21:13, HamsterofDeath <h-star [at] gmx [dot] de> wrote:
So let's make a problem: def fak(n:Int) = if ( n == 0) 1 else n *
fak(n-1) * 1.0 Oh, look, the return type wasn't Int after all! It was
Double the whole time!
>>
def fak(i:Int) = if (..) Int else Int * ignore * double

gives a double :)

Only if it can be proved that int * ignre * double gives a double. How can you demonstrate this without knowing what is being resolved for Int.*, and how can you know this without having at least a lower bound on ignore? The .* could be coming from anywhere, including an implicit conversion.
Matthew

--
Dr Matthew PocockIntegrative Bioinformatics Group, School of Computing Science, Newcastle Universitymailto: turingatemyhamster [at] gmail [dot] com gchat: turingatemyhamster [at] gmail [dot] commsn: matthew_pocock [at] yahoo [dot] co [dot] uk irc.freenode.net: drdozerskype: matthew.pococktel: (0191) 2566550mob: +447535664143
Stefan Zeiger
Joined: 2008-12-21,
User offline. Last seen 27 weeks 3 days ago.
Re: Re: Improve type inference engine

On 2012-01-03 19:11, Lars Hupel wrote:
>> Things get more interesting if you add laziness into the mix:
>>
>> def f[T](x: => T): Option[T] = None
>>
>> def g(x: Int) = f(g(x))
> A similar example without by-name parameters:
>
> def f[T](x: T): Option[T] = None
>
> def g(x: Int) = if (false) f(g(x)) else f(x)
>
> Not sure what you want to demonstrate with that. Reduction to the
> halting problem?

I gave an example where no non-recursive return path exists but the
function still returns and does not have type Nothing, so you cannot
just look at the types without considering laziness.

Your new version has two return paths: f(g(x)) and f(x). Drop the
recursive one, type-check the rest (results in Option[Int]), re-check
the whole function with that type. You get a type error, so you give up
and require an explicit type annotation (similar to
"List(1,2,3).foldRight(Nil)(_ :: _)").

-sz

H-star Development
Joined: 2010-04-14,
User offline. Last seen 2 years 26 weeks ago.
Re: Re: Improve type inference engine
let me rephrase my solution:
if (...) type(Int) else superTypeOf(int, ignore, double). still double.

now let's assume the * was actually a method of a PimpedInt:

if (...) 0 else new PimpedInt(i).pimpedMethod(x(i-1))

that problem is equal to

if (...) 0 else someMethod(x(..))

now the type of x is superTypeOf(int, return type of someMethod). if there is only one someMethod - problem solved.
if there are several, the compiler should either flag an error or pick the the that takes/can take an Int because that is what it inferred so far.

i'm pretty sure there are cases that just *cannot* be solved (brute force aside, it could just try all type permutations), no matter which algorithm you use.
the "ignore-the-unknown-algorithm" certainly does not solve chicken-egg-problems completely, but it can cover the common cases.





Am 03.01.2012 22:25, schrieb Matthew Pocock:
CAHQS_ezdhGWLp3581hRUmLwuShNXJm0r_kZABsLouERhGR8MGQ [at] mail [dot] gmail [dot] com" type="cite">

On 3 January 2012 21:13, HamsterofDeath <h-star [at] gmx [dot] de" rel="nofollow">h-star [at] gmx [dot] de> wrote:
So let's make a problem: def fak(n:Int) = if ( n == 0) 1 else n *
fak(n-1) * 1.0 Oh, look, the return type wasn't Int after all! It was
Double the whole time!
>>
def fak(i:Int) = if (..) Int else Int * ignore * double

gives a double :)

Only if it can be proved that int * ignre * double gives a double. How can you demonstrate this without knowing what is being resolved for Int.*, and how can you know this without having at least a lower bound on ignore? The .* could be coming from anywhere, including an implicit conversion.
Matthew

--
Dr Matthew Pocock Integrative Bioinformatics Group, School of Computing Science, Newcastle University mailto: turingatemyhamster [at] gmail [dot] com" target="_blank" rel="nofollow">turingatemyhamster [at] gmail [dot] com gchat: turingatemyhamster [at] gmail [dot] com" target="_blank" rel="nofollow">turingatemyhamster [at] gmail [dot] com msn: matthew_pocock [at] yahoo [dot] co [dot] uk" target="_blank" rel="nofollow">matthew_pocock [at] yahoo [dot] co [dot] uk irc.freenode.net: drdozer skype: matthew.pocock tel: (0191) 2566550 mob: +447535664143

dcsobral
Joined: 2009-04-23,
User offline. Last seen 38 weeks 5 days ago.
Re: Re: Improve type inference engine

On Tue, Jan 3, 2012 at 19:13, HamsterofDeath wrote:
> So let's make a problem: def fak(n:Int) = if ( n == 0) 1 else n *
> fak(n-1) * 1.0 Oh, look, the return type wasn't Int after all! It was
> Double the whole time!
>>>

> def fak(i:Int) = if (..) Int else Int * ignore * double
>
> gives a double :)

Says who?

class HoleInTheIdea {  def *(x: Double) = this  def *(x:
HoleInTheIdea) = this}object HoleInTheIdea {  implicit def toHole(x:
Int) = new HoleInTheIdea}

def fak(i: Int): HoleInTheIdea = if (i == 1) 1 else i * fak(i - 1) * 1.0

Oh, look, it was a HoleInTheIdea the whole time! :-)

H-star Development
Joined: 2010-04-14,
User offline. Last seen 2 years 26 weeks ago.
Re: Re: Improve type inference engine

Am 04.01.2012 00:48, schrieb Daniel Sobral:
> class HoleInTheIdea { def *(x: Double) = this def *(x:
> HoleInTheIdea) = this}object HoleInTheIdea { implicit def toHole(x:
> Int) = new HoleInTheIdea}
>
> def fak(i: Int): HoleInTheIdea = if (i == 1) 1 else i * fak(i - 1) * 1.0
that is one of the cases where inferring the type is not possible:

class HoleInTheIdea {
def *(x: Double) = this

def *(x:HoleInTheIdea) = this
}

class AnotherHoleInTheIdea {
def *(x: Double) = this

def *(x: AnotherHoleInTheIdea) = this
}

object HoleInTheIdea {
implicit def toHole(x: Int) = new HoleInTheIdea
}
object AnotherHoleInTheIdea {
implicit def toHole(x: Int) = new AnotherHoleInTheIdea
}

def fak(i: Int): AnotherHoleInTheIdea = if (i == 1) 1 else i * fak(i
- 1) * 1.0

it works for BOTH holeintheidea and anotherhole, just by changing the
return type. in such an evil, evil case, the coder has to specify his
intention.
but still, my algorithm makes a good guess in simple and non twisted
cases. i won't be implemented, but i don't care :D. i like the idea.

dcsobral
Joined: 2009-04-23,
User offline. Last seen 38 weeks 5 days ago.
Re: Re: Improve type inference engine

On Wed, Jan 4, 2012 at 17:06, HamsterofDeath wrote:
> Am 04.01.2012 00:48, schrieb Daniel Sobral:
>> class HoleInTheIdea {  def *(x: Double) = this  def *(x:
>> HoleInTheIdea) = this}object HoleInTheIdea {  implicit def toHole(x:
>> Int) = new HoleInTheIdea}
>>
>> def fak(i: Int): HoleInTheIdea = if (i == 1) 1 else i * fak(i - 1) * 1.0
> that is one of the cases where inferring the type is not possible:
>
>  class HoleInTheIdea {
>    def *(x: Double) = this
>
>    def *(x:HoleInTheIdea) = this
>  }
>
>  class AnotherHoleInTheIdea {
>    def *(x: Double) = this
>
>    def *(x: AnotherHoleInTheIdea) = this
>  }
>
>  object HoleInTheIdea {
>    implicit def toHole(x: Int) = new HoleInTheIdea
>  }
>  object AnotherHoleInTheIdea {
>    implicit def toHole(x: Int) = new AnotherHoleInTheIdea
>  }
>
>  def fak(i: Int): AnotherHoleInTheIdea  = if (i == 1) 1 else i * fak(i
> - 1) * 1.0
>
> it works for BOTH holeintheidea and anotherhole, just by changing the
> return type. in such an evil, evil case, the coder has to specify his
> intention.

You miss the point. You say that "* Double" returns Double because you
know that making fak return a Double will have that effect, but that
is just not true. If I have a code like this:

def xxx(i: Int) = if (i == 1) 1 else o.m(fak(i - 1))

Then you cannot make that guarantee any longer, because you cannot
decide "o.m" without knowing what type it is receiving. Hell, "m" may
even be a method added implicitly. I could write code that breaks to
show it, but how many times will I have to break that algorithm before
you concede it is unworkable? :-)

> but still, my algorithm makes a good guess in simple and non twisted
> cases. i won't be implemented, but i don't care :D. i like the idea.

ichoran
Joined: 2009-08-14,
User offline. Last seen 2 years 3 weeks ago.
Re: Re: Improve type inference engine
On Wed, Jan 4, 2012 at 3:48 PM, Daniel Sobral <dcsobral [at] gmail [dot] com> wrote:
On Wed, Jan 4, 2012 at 17:06, HamsterofDeath <h-star [at] gmx [dot] de> wrote:
> Am 04.01.2012 00:48, schrieb Daniel Sobral:
>> class HoleInTheIdea {  def *(x: Double) = this  def *(x:
>> HoleInTheIdea) = this}object HoleInTheIdea {  implicit def toHole(x:
>> Int) = new HoleInTheIdea}
>>
>> def fak(i: Int): HoleInTheIdea = if (i == 1) 1 else i * fak(i - 1) * 1.0
> that is one of the cases where inferring the type is not possible:
>
>  class HoleInTheIdea {
>    def *(x: Double) = this
>
>    def *(x:HoleInTheIdea) = this
>  }
>
>  class AnotherHoleInTheIdea {
>    def *(x: Double) = this
>
>    def *(x: AnotherHoleInTheIdea) = this
>  }
>
>  object HoleInTheIdea {
>    implicit def toHole(x: Int) = new HoleInTheIdea
>  }
>  object AnotherHoleInTheIdea {
>    implicit def toHole(x: Int) = new AnotherHoleInTheIdea
>  }
>
>  def fak(i: Int): AnotherHoleInTheIdea  = if (i == 1) 1 else i * fak(i
> - 1) * 1.0
>
> it works for BOTH holeintheidea and anotherhole, just by changing the
> return type. in such an evil, evil case, the coder has to specify his
> intention.

You miss the point. You say that "* Double" returns Double because you
know that making fak return a Double will have that effect, but that
is just not true. If I have a code like this:

def xxx(i: Int) = if (i == 1) 1 else o.m(fak(i - 1))

Then you cannot make that guarantee any longer, because you cannot
decide "o.m" without knowing what type it is receiving. Hell, "m" may
even be a method added implicitly. I could write code that breaks to
show it, but how many times will I have to break that algorithm before
you concede it is unworkable? :-)

What if the method is tail-recursive?

  --Rex

dcsobral
Joined: 2009-04-23,
User offline. Last seen 38 weeks 5 days ago.
Re: Re: Improve type inference engine

On Wed, Jan 4, 2012 at 19:04, Rex Kerr wrote:
>> Then you cannot make that guarantee any longer, because you cannot
>> decide "o.m" without knowing what type it is receiving. Hell, "m" may
>> even be a method added implicitly. I could write code that breaks to
>> show it, but how many times will I have to break that algorithm before
>> you concede it is unworkable? :-)
>
>
> What if the method is tail-recursive?

That's the one case I said is doable and suggested a way to do it.

ichoran
Joined: 2009-08-14,
User offline. Last seen 2 years 3 weeks ago.
Re: Re: Improve type inference engine
Sorry--I obviously haven't been following the thread closely enough!

+1 on type inference for tail-recursive methods.

(Adding type parameters on tail recursive code bothers me the most, since it adds boilerplate to an already boilerplate-heavy operation; very much makes me reach for the mutable imperative bag of tricks instead.)

  --Rex

On Wed, Jan 4, 2012 at 5:40 PM, Daniel Sobral <dcsobral [at] gmail [dot] com> wrote:
On Wed, Jan 4, 2012 at 19:04, Rex Kerr <ichoran [at] gmail [dot] com> wrote:
>> Then you cannot make that guarantee any longer, because you cannot
>> decide "o.m" without knowing what type it is receiving. Hell, "m" may
>> even be a method added implicitly. I could write code that breaks to
>> show it, but how many times will I have to break that algorithm before
>> you concede it is unworkable? :-)
>
>
> What if the method is tail-recursive?

That's the one case I said is doable and suggested a way to do it.

--
Daniel C. Sobral

I travel to the future all the time.

Copyright © 2012 École Polytechnique Fédérale de Lausanne (EPFL), Lausanne, Switzerland