How to define type lambda properly?

Question

I used =:= as example type lambda for purpose of making simple minimal example.

=:= type take two arguments, I'd like to curry one at type level.

I take naive implementation type Curry[G] = {type l[L] = L =:= G} but in practical uses it causes errors:

type X = Int
type Y = Int

type CurryInt[T] = T =:= Int
type Curry[G] = {type l[L] = L =:= G}
type CurrStatic = {type l[L] = L =:= Int}
object CurryObj {type l[L] = L =:= Int}

trait Apply[P[_], T]
implicit def liftApply[P[_], T](implicit ev : P[T]) = new Apply[P,T] {}

implicitly[Apply[CurryInt, Y]] // ok
implicitly[Apply[Curry[X]#l, Y]] // fails
implicitly[Apply[Curry[X]#l, Y]](liftApply) // fails
implicitly[Apply[Curry[X]#l, Y]](liftApply[Curry[X]#l, Y]) // ok
implicitly[Apply[CurrStatic#l, Y]] // fails
implicitly[Apply[CurryObj.l, Y]] // ok

Type inference breaks here. How should I define type lambdas to make it work?

Federico Pellegatta · Answer 1 · 2017-08-23T12:58:00.213

Consider this simplified version of your example:

trait Secret
type Curry = { type l[L] = Secret }

def foo[P[_], T](ev : P[T]) = ???
val bar: Curry#l[Int] = ???

foo(bar)

When calling foo the value bar is simply of type Secret, the compiler doesn't know from where your particular Secret comes from.

Your bar value is just a Secret, and it doesn't maintain information pointing back to Curry#l[Int].

The compiler cannot infer that P => Curry#l and T => Int.

The compiler only sees the Secret and loses the Curry#l context despite annotating the type with Curry#l[Int] instead of Secret.

Another example (coming from this question), exposing a similar behaviour:

trait Curry { type l }
trait CurryB extends Curry { type l = String }

def foo[P <: Curry](x: P#l) = ???
val bar: CurryB#l = ???

foo(bar)

CurryObj situation is different, consider that CurryInt#l, Curry#l, and CurrStatic#l are just type aliases. CurryObj.l, instead, is an actual type, part of the concrete object CurryObj.

Let's have a look to this (REPL):

scala> trait Secret
defined trait Secret

scala> type Curry = { type l[L] = Secret }
defined type alias Curry

scala> object CurryObj { type l[L] = Secret }
defined object CurryObj

scala> object S extends Secret
defined object S

scala> val foo0: Curry#l[Int] = S
foo0: Secret = S$@2c010477

scala> val foo1: CurryObj.l[Int] = S
foo1: CurryObj.l[Int] = S$@2c010477

Note that the type alias Curry#l[Int] -> Secret is resolved immediately, instead the actual type CurryObj.l[Int] is kept.

type `Curry` is like `CurrStatic` from my example. It looks very alike to `CurryObj`. Why the type information is saved in one case and losed in another? — ayvango, Aug 22 '17 at 16:10
It has meaning. But in my case `Curry#l` is used without applying `Int` to it. And `Secret` has type parameter too, so it could not be eliminated. As I had seen in `-Yinfer-debug`, type parameter is preserved but in a unusual form — ayvango, Aug 25 '17 at 06:02
Using your `Curry[G] = {type l[L] = =:=[L,G]}` the type `Curry[Int]#l` is "resolved" (it can be "eliminated") to `=:=[L, Int]` that is again incompatible with type `P[T]` of your `liftApply`. — Federico Pellegatta, Aug 25 '17 at 08:11
`L` is exactly what is needed - single unfilled "hole" in the type — ayvango, Aug 25 '17 at 10:17

score 2 · Answer 2 · answered Aug 15 '17 at 18:35

2

slightly more verbose, but compiles :) (scala 2.12.3)

  type X = Int
  type Y = Int

  type CurryInt[T] = T =:= Int
  type Curry[G] = {type l[L] = =:=[L, G]}
  type CurrStatic = {type l[L] = L =:= Int}
  object CurryObj {type l[L] = L =:= Int}

  trait Apply[P[_], T]
  implicit def liftApply[P[_], T](implicit ev : P[T]) = new Apply[P,T] {}


  type L1[R] = =:=[R, X]
  type L2[R] = =:=[R, Int]
  implicitly[Apply[CurryInt, Y]] // ok
  implicitly[Apply[L1, Y]] // ok
  implicitly[Apply[L1, Y]](liftApply[L1, Y]) // ok
  implicitly[Apply[Curry[X]#l, Y]](liftApply[Curry[X]#l, Y]) // ok
  implicitly[Apply[L2, Y]] // ok
  implicitly[Apply[CurryObj.l, Y]] // ok

answered Aug 15 '17 at 18:35

pedromss

2,443
18
24

shortly: does not use type projection. Type declaration are allowed to have unbound variables – ayvango Aug 15 '17 at 20:12
You weren't specific as to your requirements, however this solution compiles why are you trying to go with the 'type projection'? Is it just an exercicse? – pedromss Aug 15 '17 at 21:38
I was oblivious that unbound types are allowed in type expression. So I tried to encode something like `λx.λy.x==y` in type level. I could not imagine that simple `λx.x==y` would be correct scala expression. – ayvango Aug 15 '17 at 22:04
Your answer solves my specific use case replacing type lambdas with named expressions. But generally type lambdas still causes type inference errors and I could not grasp why. – ayvango Aug 15 '17 at 22:04

score 0 · Answer 3 · answered Sep 03 '17 at 19:47

It seems that scala compiler could not handle naked types from type projections. I traced -Ytyper-debug output and found that all needed type information is carried away but is rejected for no apparent reason. But it still possible to get type lambdas wrapping expressions inside a trait. That answer gave me an insight towards solution.

type X = Int
type Y = Int

trait Wrap {
  type l[T]
}
trait GenWrap[W[_]] extends Wrap {
  final type l[T] = W[T]
}

type CInt[T] = T =:= Int
class CurryInt extends Wrap {type l[T] = T =:= Int}
class Curry[U] extends Wrap {type l[T] = T =:= U}
type TCurry[U] = Wrap {type l[T] = T =:= U}

trait Apply[W <: Wrap, T]
implicit def lift[W <: Wrap, T](implicit ev : W#l[T]) = new Apply[W,T] {}

implicitly[Apply[CurryInt, Y]]
implicitly[Apply[Curry[X], Y]]
implicitly[Apply[TCurry[X], Y]]
implicitly[Apply[GenWrap[CInt], Y]]

How to define type lambda properly?

3 Answers3

Linked