Ответ 1
Обзор
Типовое программирование имеет много общего с традиционным программированием на уровне значений. Однако, в отличие от программирования на уровне значений, где вычисление происходит во время выполнения, при программировании на уровне типа вычисление происходит во время компиляции. Я попытаюсь провести параллели между программированием на уровне значений и программированием на уровне уровня.
Парадигмы
Существуют две основные парадигмы программирования типа: "объектно-ориентированный" и "функциональный". Большинство примеров, связанных с этим, следуют объектно-ориентированной парадигме.
Хороший, довольно простой пример программирования на уровне типа в объектно-ориентированной парадигме можно найти в apocalisp реализация лямбда-исчисления, реплицируется здесь:
// Abstract trait
trait Lambda {
type subst[U <: Lambda] <: Lambda
type apply[U <: Lambda] <: Lambda
type eval <: Lambda
}
// Implementations
trait App[S <: Lambda, T <: Lambda] extends Lambda {
type subst[U <: Lambda] = App[S#subst[U], T#subst[U]]
type apply[U] = Nothing
type eval = S#eval#apply[T]
}
trait Lam[T <: Lambda] extends Lambda {
type subst[U <: Lambda] = Lam[T]
type apply[U <: Lambda] = T#subst[U]#eval
type eval = Lam[T]
}
trait X extends Lambda {
type subst[U <: Lambda] = U
type apply[U] = Lambda
type eval = X
}
Как видно из примера, объектно-ориентированная парадигма для программирования на уровне типов выполняется следующим образом:
- Сначала: определить абстрактный признак с различными тегами абстрактного типа (см. ниже, для какого абстрактного поля). Это шаблон для гарантии того, что поля определенных типов существуют во всех реализациях без принудительной реализации. В примере лямбда-исчисления это соответствует
trait Lambda
, что гарантирует существование следующих типов:subst
,apply
иeval
. - Далее: определить подвыражения, которые расширяют абстрактный признак и реализовывать различные абстрактные поля
- Часто эти подзапросы будут параметризоваться с помощью аргументов. В примере лямбда-исчисления подтипы
trait App extends Lambda
, которые параметризуются двумя типами (S
иT
, оба должны быть подтипамиLambda
),trait Lam extends Lambda
, параметризованными одним типом (T
), иtrait X extends Lambda
(который не параметризуется). - поля типа часто реализуются путем обращения к параметрам типа subtrait и иногда ссылаются на их типы полей с помощью хеш-оператора:
#
(который очень похож на оператор точки:.
для значений). В примереApp
примера исчисления лямбда типeval
реализуется следующим образом:type eval = S#eval#apply[T]
. Это по существу вызывает типeval
параметра traitS
и вызываетapply
с параметромT
результата. Примечание.S
имеет типeval
, потому что параметр указывает его подтипLambda
. Аналогично, результатeval
должен иметь типapply
, поскольку он указан подтипомLambda
, как указано в абстрактном признакеLambda
.
- Часто эти подзапросы будут параметризоваться с помощью аргументов. В примере лямбда-исчисления подтипы
Функциональная парадигма состоит из определения множества конструкторов с параметризованным типом, которые не сгруппированы в свойствах.
Сравнение между программированием на уровне значений и программированием на уровне типа
- абстрактный класс
- уровень ценности:
abstract class C { val x }
- тип уровня:
trait C { type X }
- уровень ценности:
- зависимые от пути типы
-
C.x
(ссылка на значение поля/функция x в объекте C) -
C#x
(ссылка типа поля x в признаке C)
-
- подпись функции (без реализации)
- уровень ценности:
def f(x:X) : Y
- type-level:
type f[x <: X] <: Y
(это называется "конструктором типа" и обычно встречается в абстрактном признаке)
- уровень ценности:
- реализация функции
- уровень ценности:
def f(x:X) : Y = x
- тип уровня:
type f[x <: X] = x
- уровень ценности:
- условными
- проверка равенства
- уровень ценности:
a:A == b:B
- тип уровня:
implicitly[A =:= B]
- уровень ценности: происходит в JVM через unit test во время выполнения (то есть без ошибок времени выполнения):
- in essense - это утверждение:
assert(a == b)
- in essense - это утверждение:
- type-level: происходит в компиляторе с помощью typecheck (т.е. ошибок компилятора):
- по существу - это сравнение типов: например.
implicitly[A =:= B]
-
A <:< B
, компилируется, только еслиA
является подтипомB
-
A =:= B
, компилируется, только еслиA
является подтипомB
иB
является подтипомA
-
A <%< B
, ( "viewable as" ) компилируется только в том случае, еслиA
доступен для просмотра какB
(т.е. существует неявное преобразование изA
в подтипB
) - пример
- больше операторов сравнения
- по существу - это сравнение типов: например.
- уровень ценности:
Преобразование между типами и значениями
-
Во многих примерах типы, определенные с помощью признаков, часто являются абстрактными и запечатаны и поэтому не могут быть созданы напрямую или через анонимный подкласс. Поэтому обычно используется
null
как значение-заполнитель при выполнении вычисления на уровне значения с использованием какого-либо типа интереса:- например.
val x:A = null
, гдеA
- тип, который вам нужен
- например.
-
Из-за стирания типов параметризованные типы выглядят одинаково. Кроме того, (как упоминалось выше) значения, с которыми вы работаете, имеют тенденцию быть
null
, и поэтому настройка типа объекта (например, с помощью оператора соответствия) неэффективна.
Хитрость заключается в использовании неявных функций и значений. Основной случай обычно является неявным значением, а рекурсивный случай обычно является неявной функцией. В самом деле, программирование на уровне шрифтов сильно влияет на имплициты.
Рассмотрим этот пример (взятый из метаскали и apocalisp):
sealed trait Nat
sealed trait _0 extends Nat
sealed trait Succ[N <: Nat] extends Nat
Здесь у вас есть кодировка из натурального числа в peano. То есть у вас есть тип для каждого неотрицательного целого: специальный тип для 0, а именно _0
; и каждое целое число больше нуля имеет тип формы Succ[A]
, где A
- это тип, представляющий меньшее целое число. Например, тип, представляющий 2, будет следующим: Succ[Succ[_0]]
(преемник дважды применяется к типу, представляющему ноль).
Мы можем использовать различные натуральные числа для более удобной ссылки. Пример:
type _3 = Succ[Succ[Succ[_0]]]
(Это очень похоже на определение a val
как результат функции.)
Теперь предположим, что мы хотим определить функцию уровня значения def toInt[T <: Nat](v : T)
, которая принимает значение аргумента v
, которое соответствует Nat
и возвращает целое число, представляющее натуральное число, закодированное в типе v
. Например, если мы имеем значение val x:_3 = null
(null
типа Succ[Succ[Succ[_0]]]
), мы хотели бы, чтобы toInt(x)
возвращал 3
.
Чтобы реализовать toInt
, мы будем использовать следующий класс:
class TypeToValue[T, VT](value : VT) { def getValue() = value }
Как мы увидим ниже, будет создан объект, построенный из класса TypeToValue
для каждого Nat
от _0
до (например) _3
, и каждый будет хранить представление значения соответствующего типа ( т.е. TypeToValue[_0, Int]
сохранит значение 0
, TypeToValue[Succ[_0], Int]
сохранит значение 1
и т.д.). Примечание. TypeToValue
параметризуется двумя типами: T
и VT
. T
соответствует типу, который мы пытаемся присвоить значения (в нашем примере Nat
), а VT
соответствует типу присвоенного ему значения (в нашем примере Int
).
Теперь мы делаем следующие два неявных определения:
implicit val _0ToInt = new TypeToValue[_0, Int](0)
implicit def succToInt[P <: Nat](implicit v : TypeToValue[P, Int]) =
new TypeToValue[Succ[P], Int](1 + v.getValue())
И мы реализуем toInt
следующим образом:
def toInt[T <: Nat](v : T)(implicit ttv : TypeToValue[T, Int]) : Int = ttv.getValue()
Чтобы понять, как работает toInt
, рассмотрим, что он делает на нескольких входах:
val z:_0 = null
val y:Succ[_0] = null
Когда мы вызываем toInt(z)
, компилятор ищет неявный аргумент ttv
типа TypeToValue[_0, Int]
(так как z
имеет тип _0
). Он находит объект _0ToInt
, он вызывает метод getValue
этого объекта и возвращается 0
. Важно отметить, что мы не указывали программе, для которой объект использовать, компилятор нашел это неявно.
Теперь рассмотрим toInt(y)
. На этот раз компилятор ищет неявный аргумент ttv
типа TypeToValue[Succ[_0], Int]
(так как y
имеет тип Succ[_0]
). Он находит функцию succToInt
, которая может возвращать объект соответствующего типа (TypeToValue[Succ[_0], Int]
) и оценивает его. Сама эта функция принимает неявный аргумент (v
) типа TypeToValue[_0, Int]
(т.е. A TypeToValue
, где параметр первого типа имеет меньше Succ[_]
). Компилятор поставляет _0ToInt
(как это было сделано при оценке toInt(z)
выше), а succToInt
создает новый объект TypeToValue
со значением 1
. Опять же, важно отметить, что компилятор предоставляет все эти значения неявно, поскольку у нас нет доступа к ним явно.
Проверка вашей работы
Существует несколько способов проверить, что ваши вычисления на уровне типа делают то, что вы ожидаете. Вот несколько подходов. Сделайте два типа A
и B
, которые вы хотите проверить, равны. Затем проверьте, что следующая компиляция:
-
Equal[A, B]
- с: trait
Equal[T1 >: T2 <: T2, T2]
(взято из apocolisp)
- с: trait
-
implicitly[A =:= B]
В качестве альтернативы вы можете преобразовать тип в значение (как показано выше) и выполнить проверку значений времени. Например. assert(toInt(a) == toInt(b))
, где A
имеет тип A
и B
имеет тип B
.
Дополнительные ресурсы
Полный набор доступных конструкций можно найти в разделе типов справочного руководства scala (pdf).
Adriaan Moors содержит несколько научных статей о конструкторах типов и связанных с ними темах с примерами из scala:
- Дженерики высшего сорта (pdf)
- Тип Полиморфизм конструктора для scala: Теория и практика (pdf) (кандидатская диссертация, в которую включена предыдущая работа мавров)
- Вывод полиморфизма типа конструктора
Apocalisp - это блог со многими примерами программирования на уровне типа в scala.
- Программирование на уровне в Scala - это фантастическая экскурсия по программированию на каком-то уровне, включающая логические значения, натуральные числа (как указано выше), двоичные числа, гетерогенные списки и т.д.
- Подробнее scala Typehackery - это реализация исчисления лямбда выше.
ScalaZ - очень активный проект, который предоставляет функциональность, которая расширяет API scala, используя различные функции программирования на уровне уровня. Это очень интересный проект, который имеет большое значение.
MetaScala - это библиотека уровня типа для Scala, включая мета-типы для натуральных чисел, булевых элементов, единиц, HList и т.д. Это проект Jesper Nordenberg (его блог).
Michid (blog) содержит несколько удивительных примеров программирования на уровне типа в scala (из другого ответа):
- Мета-программирование с помощью scala Часть I: Дополнение
- Мета-программирование с помощью scala Часть II: Умножение
- Мета-программирование с помощью scala Часть III: Приложение с частичной функцией
- Мета-программирование с помощью scala: условная компиляция и развертка цикла
- Scala кодировка уровня уровня исчисления SKI
У Debasish Ghosh (blog) есть также некоторые соответствующие должности:
- Абстракции более высокого порядка в Scala
- Статическая типизация дает вам начало
- Scala подразумевает классы типов, здесь я прихожу
- Рефакторинг в классы scala
- Использование ограничений обобщенного типа
- Как системные слова типа scalas для вас
- Выбор между членами абстрактного типа
(Я занимался некоторыми исследованиями по этому предмету, и вот что я узнал. Я все еще новичок в этом, поэтому, пожалуйста, укажите любые неточности в этом ответе.)