blob: 27090989883b43e55a0d1ca20cbb9986de721bb1 (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
|
sealed trait Nat {
type IsZero[U, A <: U, B <: U] <: U
}
final object Zero extends Nat {
type IsZero[U, T <: U, F <: U] = T
}
final class Succ[N <: Nat] extends Nat {
type IsZero[U, T <: U, F <: U] = F
}
trait HList {
type Head
type Tail <: HList
type Drop[N <: Nat] = N#IsZero[HList, this.type, Tail]
type Apply[N <: Nat] = Drop[N]#Head // typechecks as HList.this.Head
}
object Test {
type ::[H, T <: HList] = HList { type Head = H; type Tail = T}
type HNil <: HList
type T = Int :: String :: HNil
type U = T#Drop[Succ[Zero.type]]#Head
type V = T#Apply[Succ[Zero.type]]
var u: U = ???
var v: V = ???
u = v
}
|
