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/ |
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/ > |
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/ >> > > |
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/ > >> > > > > |
Powered by Nabble | Edit this page |