Type-Level Programming Problem

[Daniel Kröni]

Hi all,
I'm working through "Type-Level Programming in Scala" [0] and this
stuff is just amazing! But while experimenting by myself I hit a
problem.
Here is a contrived version of the problematic code: (The Bool stuff
is copied from [1])

sealed trait Bool {
 // If True then T else F
 type If[T <: Up, F <: Up, Up] <: Up
}

sealed trait True extends Bool {
 type If[T <: Up, F <: Up, Up] = T
}
sealed trait False extends Bool {
 type If[T <: Up, F <: Up, Up] = F
}

object BoolTest {

 class B[BB <: Bool]
 // This definition works fine
 class ![BB <: Bool] extends B[BB#If[False, True, Bool]] // YYY

 // But I want something like this!
 // class ![BB <: Bool] extends B[BB#If[False, True, Bool]#If[True,
False, Bool]] // XXX

 def main(args: Array[String]) {
   val b0: B[True] = new B[True]
   val b1: ![False] = new ![False]
   val b2: B[True] = new ![False] // Problem is here if line XXX is active

   // This works as expected
   implicitly[False#If[False, True, Bool]#If[True, False, Bool] =:= True]

   /* The following two lines compile with YYY but not with XXX
   implicitly[![False] <:< B[True]]
   implicitly[![True] <:< B[True#If[False, True, Bool]#If[True, False, Bool]]]
   */
 }
}


Aren't the resulting types from " BB#If[False, True, Bool] " and  "
BB#If[False, True, Bool]#If[True, False, Bool] " identical?

Any help would be appreciated!
Thanks Daniel


[0] http://apocalisp.wordpress.com/2010/06/08/type-level-programming-in-scala/
[1] http://apocalisp.wordpress.com/2010/06/13/type-level-programming-in-scala-part-3-boolean/

[Mark Harrah]

Hi Daniel,

On Mon, 10 Jan 2011 14:14:07 +0100
Daniel Kröni <[hidden email]> wrote:

> Hi all,
> I'm working through "Type-Level Programming in Scala" [0] and this
> stuff is just amazing! But while experimenting by myself I hit a
> problem.
> Here is a contrived version of the problematic code: (The Bool stuff
> is copied from [1])
>
> sealed trait Bool {
>  // If True then T else F
>  type If[T <: Up, F <: Up, Up] <: Up
> }
>
> sealed trait True extends Bool {
>  type If[T <: Up, F <: Up, Up] = T
> }
> sealed trait False extends Bool {
>  type If[T <: Up, F <: Up, Up] = F
> }
>
> object BoolTest {
>
>  class B[BB <: Bool]
>  // This definition works fine
>  class ![BB <: Bool] extends B[BB#If[False, True, Bool]] // YYY
>
>  // But I want something like this!
>  // class ![BB <: Bool] extends B[BB#If[False, True, Bool]#If[True,
> False, Bool]] // XXX
>
>  def main(args: Array[String]) {
>    val b0: B[True] = new B[True]
>    val b1: ![False] = new ![False]
>    val b2: B[True] = new ![False] // Problem is here if line XXX is active
>
>    // This works as expected
>    implicitly[False#If[False, True, Bool]#If[True, False, Bool] =:= True]
>
>    /* The following two lines compile with YYY but not with XXX
>    implicitly[![False] <:< B[True]]
>    implicitly[![True] <:< B[True#If[False, True, Bool]#If[True, False, Bool]]]
>    */
>  }
> }
>
>
> Aren't the resulting types from " BB#If[False, True, Bool] " and  "
> BB#If[False, True, Bool]#If[True, False, Bool] " identical?

http://lampsvn.epfl.ch/trac/scala/ticket/3443

Unfortunately (for type-level programming) the change described there was intentional and makes type-level things difficult.

-Mark

> Any help would be appreciated!
> Thanks Daniel
>
>
> [0] http://apocalisp.wordpress.com/2010/06/08/type-level-programming-in-scala/
> [1] http://apocalisp.wordpress.com/2010/06/13/type-level-programming-in-scala-part-3-boolean/
>

[Daniel Kröni]

This is really unfortunate! I trusted the slogan: "towards equal rights for higher-kinded types".
Here is my balanced tree where the balanced property is statically enforced:


sealed trait BTree[A, H <: Nat] // H is height of the tree
sealed case class Leaf[A](a: A) extends BTree [A, _0]
sealed case class Branch[A, HL <: Nat, HR <: Nat](l: BTree[A, HL], v: A, r: BTree[A, HR])
                                                (implicit y: HL#Diff[HR]#Compare[_1]#le =:= True) // guards against unbalanced construction
                                                  extends BTree [A, Succ[HL#Max[HR]]]

object BTreeTest {
 def main(args: Array[String]) {
   val ok_1 =  Branch(  Leaf(3), 5,  Leaf(3))
   val ok_2 = Branch(Leaf(3), 4, ok_1)
   val ok_3 = Branch(ok_1, 4, ok_1)

   //val unbalanced = Branch(Leaf(1), 3, ok_2) // unbalanced: does not compile!
 }
}

I would have preferred to place the Max type function in the Nat object like this:

object Nat {

  type Max[N <: Nat, M <: Nat] = N#Compare[M]#ge#If[N,M, Nat] // reusing your compare code

}

or express it directly in the extends as shown below. 

... class Branch ... extends BTree [A, Succ[HL#Compare[HR]#gt#If[HL,HR, Nat]]] 

But instead I had to implement it on the Nat (sub-)traits like this:

// Most of the code bellow is borrowed from http://apocalisp.wordpress.com/2010/06/08/type-level-programming-in-scala/

// and https://github.com/harrah/up/blob/master/LICENSE applies (I hope I got that right)

sealed trait Nat {

  type Match[NonZero[N <: Nat] <: Up, IfZero <: Up, Up] <: Up

  type Compare[N <: Nat] <: Comparison

  type Diff[O <: Nat] <: Nat // computes the absolute difference between this and O

  type Max[O <: Nat] <: Nat // API

  type _Max[O <: Nat, THIS <: Nat, OTHER <: Nat] <: Nat // Ugly implementation

}

sealed trait _0 extends Nat {

  type Match[NonZero[N <: Nat] <: Up, IfZero <: Up, Up] = IfZero

  // Type lambdas look fancier than "type ConstLT[A] = LT". What do you think?

  type Compare[N <: Nat] = N#Match[({type λ[α] = LT})#λ, EQ, Comparison]

  

  type Max[O <: Nat] = _Max[O, _0, O]

  type _Max[O <: Nat, THIS <: Nat, OTHER <: Nat] = OTHER

  type Diff[O <: Nat] = O

}

sealed trait Succ[N <: Nat] extends Nat {

  type Match[NonZero[_ <: Nat] <: Up, IfZero <: Up, Up] = NonZero[N]

  type Compare[O <: Nat] = O#Match[N#Compare, GT, Comparison]

  type Max[O <: Nat] = _Max[O, Succ[N], O]

  type  _Max[O <: Nat, THIS <: Nat, OTHER <: Nat] = O#Match[({ type λ[α <: Nat] = N#_Max[α, THIS, OTHER]})#λ, THIS, Nat]

  type Diff[O <: Nat] = O#Match[N#Diff, Succ[N], Nat]

}

I think it's pretty nice to have properties like "balancedness" statically guaranteed and it would be a shame to not support that idea.

I must admit that I don't understand Martin's statement in #3443 but I also think that you are the one to provide the one-by-one argument he asked for. Did he ever answer to your last comment?

Anyway, thanks for your blog series.

Daniel



On Mon, Jan 17, 2011 at 4:45 PM, Mark Harrah <[hidden email]> wrote:
> Hi Daniel,
>
> On Mon, 10 Jan 2011 14:14:07 +0100
> Daniel Kröni <[hidden email]> wrote:
>
>> Hi all,
>> I'm working through "Type-Level Programming in Scala" [0] and this
>> stuff is just amazing! But while experimenting by myself I hit a
>> problem.
>> Here is a contrived version of the problematic code: (The Bool stuff
>> is copied from [1])
>>
>> sealed trait Bool {
>>  // If True then T else F
>>  type If[T <: Up, F <: Up, Up] <: Up
>> }
>>
>> sealed trait True extends Bool {
>>  type If[T <: Up, F <: Up, Up] = T
>> }
>> sealed trait False extends Bool {
>>  type If[T <: Up, F <: Up, Up] = F
>> }
>>
>> object BoolTest {
>>
>>  class B[BB <: Bool]
>>  // This definition works fine
>>  class ![BB <: Bool] extends B[BB#If[False, True, Bool]] // YYY
>>
>>  // But I want something like this!
>>  // class ![BB <: Bool] extends B[BB#If[False, True, Bool]#If[True,
>> False, Bool]] // XXX
>>
>>  def main(args: Array[String]) {
>>    val b0: B[True] = new B[True]
>>    val b1: ![False] = new ![False]
>>    val b2: B[True] = new ![False] // Problem is here if line XXX is active
>>
>>    // This works as expected
>>    implicitly[False#If[False, True, Bool]#If[True, False, Bool] =:= True]
>>
>>    /* The following two lines compile with YYY but not with XXX
>>    implicitly[![False] <:< B[True]]
>>    implicitly[![True] <:< B[True#If[False, True, Bool]#If[True, False, Bool]]]
>>    */
>>  }
>> }
>>
>>
>> Aren't the resulting types from " BB#If[False, True, Bool] " and  "
>> BB#If[False, True, Bool]#If[True, False, Bool] " identical?
>
> http://lampsvn.epfl.ch/trac/scala/ticket/3443
>
> Unfortunately (for type-level programming) the change described there was intentional and makes type-level things difficult.
>
> -Mark
>
>> Any help would be appreciated!
>> Thanks Daniel
>>
>>
>> [0] http://apocalisp.wordpress.com/2010/06/08/type-level-programming-in-scala/
>> [1] http://apocalisp.wordpress.com/2010/06/13/type-level-programming-in-scala-part-3-boolean/
>>
>
>

[Mark Harrah]

On Tue, 18 Jan 2011 15:03:54 +0100
Daniel Kröni <[hidden email]> wrote:

> This is really unfortunate! I trusted the slogan: "towards equal rights for
> higher-kinded types".

Yes, I agree it is unfortunate.  Your issue with is type projections, not higher-kinded types, though.

> Here is my balanced tree where the balanced property is statically enforced:

Neat.

> sealed trait BTree[A, H <: Nat] // H is height of the tree
> sealed case class Leaf[A](a: A) extends BTree [A, _0]
> sealed case class Branch[A, HL <: Nat, HR <: Nat](l: BTree[A, HL], v: A, r:
> BTree[A, HR])
>                                                 (implicit y:
> HL#Diff[HR]#Compare[_1]#le =:= True) // guards against unbalanced
> construction
>                                                   extends BTree [A,
> Succ[HL#Max[HR]]]
>
> object BTreeTest {
>  def main(args: Array[String]) {
>    val ok_1 =  Branch(  Leaf(3), 5,  Leaf(3))
>    val ok_2 = Branch(Leaf(3), 4, ok_1)
>    val ok_3 = Branch(ok_1, 4, ok_1)
>
>    //val unbalanced = Branch(Leaf(1), 3, ok_2) // unbalanced: does not
> compile!
>  }
> }
>
> I would have preferred to place the Max type function in the Nat object like
> this:
>
> object Nat {
>   type Max[N <: Nat, M <: Nat] = N#Compare[M]#ge#If[N,M, Nat] // reusing
> your compare code
> }
>
> or express it directly in the extends as shown below.
> ... class Branch ... extends BTree [A, Succ[HL#Compare[HR]#gt#If[HL,HR,
> Nat]]]
>
> But instead I had to implement it on the Nat (sub-)traits like this:

Right, while at least you can work around it, everyone has to have their own Nat that they can extend.

> // Most of the code bellow is borrowed from
> http://apocalisp.wordpress.com/2010/06/08/type-level-programming-in-scala/
> // and https://github.com/harrah/up/blob/master/LICENSE applies (I hope I
> got that right)

Yup, new BSD license.  I'd be happy to include in the original up project anything you come up with and/or post any writeup you'd like to make on it.  I'm pretty sure anyone who read the series would appreciate your work.

> sealed trait Nat {
>   type Match[NonZero[N <: Nat] <: Up, IfZero <: Up, Up] <: Up
>   type Compare[N <: Nat] <: Comparison
>
>   type Diff[O <: Nat] <: Nat // computes the absolute difference between
> this and O
>
>   type Max[O <: Nat] <: Nat // API
>   type _Max[O <: Nat, THIS <: Nat, OTHER <: Nat] <: Nat // Ugly
> implementation
> }
> sealed trait _0 extends Nat {
>   type Match[NonZero[N <: Nat] <: Up, IfZero <: Up, Up] = IfZero
>   // Type lambdas look fancier than "type ConstLT[A] = LT". What do you
> think?
>   type Compare[N <: Nat] = N#Match[({type λ[α] = LT})#λ, EQ, Comparison]
>
>   type Max[O <: Nat] = _Max[O, _0, O]
>   type _Max[O <: Nat, THIS <: Nat, OTHER <: Nat] = OTHER
>
>   type Diff[O <: Nat] = O
> }
>
> sealed trait Succ[N <: Nat] extends Nat {
>   type Match[NonZero[_ <: Nat] <: Up, IfZero <: Up, Up] = NonZero[N]
>   type Compare[O <: Nat] = O#Match[N#Compare, GT, Comparison]
>
>   type Max[O <: Nat] = _Max[O, Succ[N], O]
>   type  _Max[O <: Nat, THIS <: Nat, OTHER <: Nat] = O#Match[({ type λ[α <:
> Nat] = N#_Max[α, THIS, OTHER]})#λ, THIS, Nat]
>
>   type Diff[O <: Nat] = O#Match[N#Diff, Succ[N], Nat]
> }
>
>
> I think it's pretty nice to have properties like "balancedness" statically
> guaranteed and it would be a shame to not support that idea.

Sure, although there are tradeoffs when doing too much type-level computation in Scala.  It would be interesting to compare the compile time with a normal implementation, for example.

> I must admit that I don't understand Martin's statement in #3443 but I also
> think that you are the one to provide the one-by-one argument he asked for.
> Did he ever answer to your last comment?

http://scala-programming-language.1934581.n4.nabble.com/scala-2-8-spec-clarification-td2226275.html

> Anyway, thanks for your blog series.

Thanks for doing something interesting with it!

-Mark

> Daniel
>
>
>
> On Mon, Jan 17, 2011 at 4:45 PM, Mark Harrah <[hidden email]> wrote:
> > Hi Daniel,
> >
> > On Mon, 10 Jan 2011 14:14:07 +0100
> > Daniel Kröni <[hidden email]> wrote:
> >
> >> Hi all,
> >> I'm working through "Type-Level Programming in Scala" [0] and this
> >> stuff is just amazing! But while experimenting by myself I hit a
> >> problem.
> >> Here is a contrived version of the problematic code: (The Bool stuff
> >> is copied from [1])
> >>
> >> sealed trait Bool {
> >>  // If True then T else F
> >>  type If[T <: Up, F <: Up, Up] <: Up
> >> }
> >>
> >> sealed trait True extends Bool {
> >>  type If[T <: Up, F <: Up, Up] = T
> >> }
> >> sealed trait False extends Bool {
> >>  type If[T <: Up, F <: Up, Up] = F
> >> }
> >>
> >> object BoolTest {
> >>
> >>  class B[BB <: Bool]
> >>  // This definition works fine
> >>  class ![BB <: Bool] extends B[BB#If[False, True, Bool]] // YYY
> >>
> >>  // But I want something like this!
> >>  // class ![BB <: Bool] extends B[BB#If[False, True, Bool]#If[True,
> >> False, Bool]] // XXX
> >>
> >>  def main(args: Array[String]) {
> >>    val b0: B[True] = new B[True]
> >>    val b1: ![False] = new ![False]
> >>    val b2: B[True] = new ![False] // Problem is here if line XXX is
> active
> >>
> >>    // This works as expected
> >>    implicitly[False#If[False, True, Bool]#If[True, False, Bool] =:= True]
> >>
> >>    /* The following two lines compile with YYY but not with XXX
> >>    implicitly[![False] <:< B[True]]
> >>    implicitly[![True] <:< B[True#If[False, True, Bool]#If[True, False,
> Bool]]]
> >>    */
> >>  }
> >> }
> >>
> >>
> >> Aren't the resulting types from " BB#If[False, True, Bool] " and  "
> >> BB#If[False, True, Bool]#If[True, False, Bool] " identical?
> >
> > http://lampsvn.epfl.ch/trac/scala/ticket/3443
> >
> > Unfortunately (for type-level programming) the change described there was
> intentional and makes type-level things difficult.
> >
> > -Mark
> >
> >> Any help would be appreciated!
> >> Thanks Daniel
> >>
> >>
> >> [0]
> http://apocalisp.wordpress.com/2010/06/08/type-level-programming-in-scala/
> >> [1]
> http://apocalisp.wordpress.com/2010/06/13/type-level-programming-in-scala-part-3-boolean/
> >>
> >
> >