Обзор
программирование Тип уровня имеет много общего с традиционным, значение уровня программирования. Однако, в отличие от программирования на уровне значений, где вычисление происходит во время выполнения, при программировании на уровне типа вычисление происходит во время компиляции. Я попытаюсь провести параллели между программированием на уровне ценности и программированием на уровне уровня.
Парадигмы
Существуют две основные парадигмы в программировании типа уровня: «объектно-ориентированный» и «функциональный». Большинство примеров, связанных с этим, следуют объектно-ориентированной парадигме.
Хороший, довольно простой пример программирования типа уровня в объектно-ориентированной парадигмы можно найти в apocalisp-х implementation of the lambda calculus, реплицируются здесь:
// 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.
- Далее: определить subtraits, которые расширяют абстрактные черты и реализовать различные абстрактные поля типа
- Часто эти subtraits будут параметрироваться с аргументами. В примере лямбда-исчислении, подтипы являются
trait App extends Lambda, которые спараметрирован с двумя типами (S и T, оба должны быть подтипы Lambda), trait Lam extends Lambda параметризованные с одним типом (T) и trait X extends Lambda (который не является параметризованных).
- поля типа часто реализуются путем ссылки на параметры типа subtrait и иногда ссылаются на их поля типа с помощью оператора хеша:
# (который очень похож на оператор точки: . для значений). В примере примера лямбда-исчисления тип eval реализован следующим образом: type eval = S#eval#apply[T]. Это по существу вызывает тип eval параметра признака S и вызывает apply с параметром T на результат. Примечание. S имеет тип eval, потому что параметр указывает его подтип Lambda. Аналогично, результат eval должен иметь тип apply, поскольку он указан подтипом Lambda, как указано в абстрактном признаке Lambda.
Функциональная парадигма состоит в определении много параметризованных конструкторов типов, которые не группируются в черты.
Сравнение между программированием значения уровня и программирования типа уровня
- abstract class
- значение уровня:
abstract class C { val x }
- уровень типа:
trait C { type X }
- путь зависит типы
C.x (ссылки на значение поля/функцию х в объекте C)C#x (ссылки на тип поля х в признаке C)
- функция подпись (без реализации)
- значение уровня :
def f(x:X) : Y
- Тип уровня:
type f[x <: X] <: Y (это называется конструктором типа и обычно встречается в абстрактном признаке)
- реализация функции
- значение уровня:
def f(x:X) : Y = x
- уровень типа:
type f[x <: X] = x
- условными
- проверки равенства
- значение уровня:
a:A == b:B
- уровень типа:
implicitly[A =:= B]
- значение уровня: Случается в виртуальной машине Java с помощью теста блока во время выполнения (т.е. нет ошибок во время выполнения):
- в Ессенции не является утверждают:
assert(a == b)
- уровень типа: Случается в компиляторе через typecheck (т.е. без ошибок компилятора):
- по сути является сравнение типов: например
implicitly[A =:= B]
A <:< B, компилирует только если A является подтипом BA =:= B, компилирует только если A является подтипом B и B является подтипом AA <%< B, («видимыми как») компилирует только если A можно просмотреть как B (т.е.существует неявное преобразование из A к подтипу B)- an example
- more comparison operators
Преобразование между типами и значения
Во многих из экс Ярлыки, типы, определенные через признаки, часто являются абстрактными и запечатаны, и поэтому не могут быть созданы напрямую или через анонимный подкласс. Таким образом, он является общим для использования null в качестве значения заполнителя при выполнении вычисления значения уровня, используя некоторый тип интереса:
- например
val x:A = null, где A типа вы заботитесь о
Благодаря типа стирания, параметризованные типы все выглядят одинаково. Кроме того, (как упоминалось выше) значения, с которыми вы работаете, имеют тенденцию быть null, и поэтому настройка типа объекта (например, через оператор соответствия) неэффективна.
Хитрость заключается в использовании неявных функций и значений. Основной случай обычно является неявным значением, а рекурсивный случай обычно является неявной функцией. Действительно, программирование на уровне шрифтов сильно использует имплициты.
Рассмотрим пример (taken from metascala и apocalisp):
sealed trait Nat
sealed trait _0 extends Nat
sealed trait Succ[N <: Nat] extends Nat
Здесь у вас есть Пеано кодирование натуральных чисел. То есть у вас есть тип для каждого неотрицательного целого: специальный тип для 0, а именно _0; и каждое целое число больше нуля имеет тип формы Succ[A], где A - это тип, представляющий меньшее целое число. Например, тип, представляющий 2, будет: Succ[Succ[_0]] (преемник дважды применяется к типу, представляющему ноль).
Мы можем использовать различные натуральные номера для более удобного обращения. Пример:
type _3 = Succ[Succ[Succ[_0]]]
(. Это очень похоже на определении 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] (то есть TypeToValue, где параметр первого типа имеет одно меньшее Succ[_]). Компилятор поставляет _0ToInt (как это было сделано при оценке toInt(z) выше), а succToInt создает новый объект TypeToValue со значением 1. Опять же, важно отметить, что компилятор предоставляет все эти значения неявно, поскольку у нас нет доступа к ним явно.
Проверка вашей работы
Есть несколько способов, чтобы убедиться, что ваши вычисления на уровне типа делают то, что вы ожидаете. Вот несколько подходов. Сделайте два типа A и B, которые вы хотите проверить, равны.Затем проверьте, что следующий компиляции:
Equal[A, B]
implicitly[A =:= B]
В качестве альтернативы, вы можете преобразовать тип в значение (как показано выше) и выполнить проверку значений времени. Например. assert(toInt(a) == toInt(b)), где a имеет тип A и b имеет тип B.
Дополнительные ресурсы
Полный набор доступных конструкций можно найти в разделе Типы the scala reference manual (pdf).
Adriaan Moors имеет несколько научных статей о конструкторах типа и связанные с ними темы с примерами из Скале:
Apocalisp - это блог со многими примерами профессионального уровня грамматический определенный член в scala.
- Type-Level Programming in Scala фантастическая экскурсия некоторого программирования типа уровня, который включает булевы, натуральные числа (как указано выше), двоичные числа, гетерогенные списки и многое другое.
- More Scala Typehackery это реализация исчисления лямбда выше.
ScalaZ - очень активный проект, предоставляющий функциональность, которая расширяет Scala API, используя различные функции программирования уровня. Это очень интересный проект, который имеет большое значение.
MetaScala - это библиотека уровня уровня для Scala, включая мета-типы для натуральных чисел, булевых единиц, единиц, HList и т. Д. Это проект Jesper Nordenberg (his blog).
Michid (blog) имеет некоторые удивительные примеры программирования типа уровня в Scala (из других ответов):
Debasish Ghosh (blog) имеет некоторые соответствующие должности, а также:
(Я занимался некоторыми исследованиями по этому вопросу, и вот что я узнал. Я еще новичок в этом, поэтому, пожалуйста, указать на какую-либо неточность в этом ответе.)
Сообщество wiki? –
Лично я считаю, что кто-то, кто хочет заниматься программированием на уровне уровня в Scala, уже знает, как сделать программирование в Scala вполне разумным. Даже если это означает, что я не понимаю ни слова тех статей, которые вы связали с :-) –