This page is no longer maintained — Please continue to the home page at

Re: Type soundness hole arising from "type lambdas"?

No replies
Kris Nuttycombe
Joined: 2009-01-16,
User offline. Last seen 42 years 45 weeks ago.
I guess that makes sense; it just seems strange to think of String as an instance of M[String], but since M is a type level function I suppose it must be.
On Wed, Sep 21, 2011 at 2:52 PM, Heiko Seeberger <heiko [dot] seeberger [at] googlemail [dot] com> wrote:
Why should that be unsound? You define a type level function X[Y] and then ignore the argument by returning E which is not related to Y.Just the same like def foo[A](a: A) = "bar", which will work for any A.

Heiko Seeberger
Twitter: hseeberger
Company: Typesafe - Enterprise-Grade Scala from the Experts
Author of Durchstarten mit Scala, a German tutorial-style Scala book

On Sep 21, 2011, at 10:44 PM, Kris Nuttycombe wrote:
[knuttycombe@floorshow ~]$ scalaWelcome to Scala version (Java HotSpot(TM) 64-Bit Server VM, Java 1.6.0_26). Type in expressions to have them evaluated.Type :help for more information.
scala> class A[B, M[_]](m: M[B])defined class A
scala> class C[E](m: E) extends A[String, ({type X[Y] = E})#X](m)defined class C
scala> new C("hi")res0: C[java.lang.String] = C@243a0589

This seems unsound to me. Can somebody explain why this is not a compile error?

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