Возможно ли использовать члены типа для уменьшения детализации типов в Scala?

Итак, это может звучать как общий вопрос о дизайне языка, но я думаю, что здесь есть что-то конкретное. В частности, я заинтересован в том, какие технические проблемы мешают неуклюжему коду, который следует, быть в целом полезным.

Все мы знаем, что «вывод типов в Scala не так хорош, как в Haskell», и что есть много причин, по которым он не может быть таким же хорошим, но при этом делать все то, что делает Scala. Но что также становится очевидным после достаточно долгого программирования на Scala, так это то, что плохой вывод типов на самом деле не так уж и плох, как многословие, необходимое для определения некоторых распространенных типов. Так, например, в полиморфной функции tail

def tail[A](ls: List[A]) =
    ls match {
        case Nil     => sys.error("Empty list")
        case x :: xs => xs
    }

необходимо явно указать параметр типа, чтобы сделать метод полезным; никак не обойти это. tail(ls: List[Any])не будет работать, потому что Scala не может понять, что тип результата совпадает с типом ввода, хотя для человека это «очевидно».

Итак, вдохновленный этой трудностью и зная, что Scala иногда может быть умнее с членами типа , чем с параметрами типа,Я написал версию List, в которой используются элементы типа :

sealed trait TMList {
    self =>
    type Of
    def :::(x: Of) = new TMCons {
        type Of = self.Of
        val head = x
        val tail = (self: TMList { type Of = self.Of })
    }
}
abstract class TMNil extends TMList
def ATMNil[A] = new TMNil { type Of = A }
abstract class TMCons extends TMList {
    self =>
    val head: Of
    val tail: TMList { type Of = self.Of }
}

. Хорошо, определение выглядит ужасно , но оно, по крайней мере, прямолинейно и позволяет нам написать наш tailметод следующим образом:

def tail4(ls: TMList) =
    ls match {
        case _: TMNil => sys.error("Empty list")
        case c: TMCons with ls.type => c.tail
    }

И красота в том, что это работает , поэтому мы можем написать (с head, определенным так, как вы ожидаете)

val ls = 1 ::: 2 ::: ATMNil
val a = tail4(ls)
println(head4(a) * head4(a))

и Scala знает , что член выходного типа по-прежнему Int. Нам пришлось написать что-то немного смешное с TMCons with ls.type, и Scala жалуется, что совпадение не является исчерпывающим, но этот фрагмент кода мог быть просто вставлен Scala для нас, потому что, конечно, когда вы сопоставляете на lsлюбой случай должно быть ls.type, и, конечно, совпадение является исчерпывающим.

Итак, мой вопрос: :в чем подвох? Почему бы нам не сделать все наши полиморфные типы таким же образом и просто изменить язык, чтобы синтаксис не выглядел так плохо? С какими техническими проблемами мы столкнемся?

Ясно, что существует проблема, заключающаяся в том, что класс не может быть ковариантным в своих членах типа; но меня это не так интересует; Я думаю, это отдельная тема. Предположим на данный момент, что нас не волнует дисперсия. Что еще может пойти не так?

Я подозреваю, что это может создать новые проблемы для вывода типов (, например, как мне пришлось определить ATMNilдля работы примера ), но я недостаточно хорошо понимаю вывод типов Scala, чтобы знать, что это будет.

редактировать, чтобы ответить на 0__:Я думаю, вы, возможно, нашли его. Версия с параметром типа работает,

def move2[A](a: TMList { type Of = A }, b: TMList { type Of = A }) = b match {
    case c: TMCons with b.type => c.head ::: a
    case _                     => a
}

Но интересно то, что без явного возвращаемого типа каррированная зависимо типизированная версия не:

def move3(a: TMList)(b: TMList { type Of = a.Of }) = b match {
    case c: TMCons with b.type => c.head ::: a
    case _                     => a
}

Scala определяет возвращаемый тип как TMList; это есть верхняя граница двух типов случая, TMList { type Of = a.Of }и a.type. Конечно, TMList { type Of = a.Of }также будет верхней границей (и той, которую я хочу, поэтому добавление явного возвращаемого типа работает )и, я думаю, более конкретная верхняя граница. Интересно, почему Scala не выводит более конкретную верхнюю границу.