Ресурсы программирования типа Scala

Согласно этому вопросу, система типов Скалы является полной по Тьюрингу. Какие ресурсы доступны, что позволяет новичку воспользоваться возможностями программирования на уровне типов?

Вот ресурсы, которые я нашел до сих пор:

Эти ресурсы великолепны, но я чувствую, что мне не хватает основ, и поэтому у меня нет прочной основы, на которой можно строить. Например, где есть введение в определения типов? Какие операции я могу выполнять над типами?

Есть ли хорошие вводные ресурсы?

Источник

5 ответов

Решение

обзор

Программирование на уровне типов имеет много общего с традиционным программированием на уровне значений. Однако, в отличие от программирования на уровне значений, где вычисления выполняются во время выполнения, в программировании на уровне типов вычисления выполняются во время компиляции. Я попытаюсь провести параллели между программированием на уровне значений и программированием на уровне типов.

парадигмы

В программировании на уровне типов есть две основные парадигмы: "объектно-ориентированная" и "функциональная". Большинство примеров, связанных с этим, следуют объектно-ориентированной парадигме.

Хороший, довольно простой пример программирования на уровне типов в объектно-ориентированной парадигме можно найти в реализации апокалипсиса лямбда-исчисления, воспроизведенной здесь:

// 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 (который не параметризован).
    • поля типа часто реализуются путем обращения к параметрам типа вычитания и иногда ссылки на их поля типа через оператор хеширования: # (что очень похоже на оператор точки: . для ценностей). В черту App примера лямбда-исчисления, тип eval реализован следующим образом: type eval = S#eval#apply[T], По сути это называется eval тип параметра признака S и звонит 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 f[x <: X] <: Y (это называется "конструктор типов" и обычно встречается в абстрактной черте)
  • реализация функции
    • Значение уровня: def f(x:X) : Y = x
    • уровень типа: type f[x <: X] = x
  • условными
  • проверка равенства
    • Значение уровня: a:A == b:B
    • уровень типа: implicitly[A =:= B]
    • уровень значения: происходит в JVM через модульное тестирование во время выполнения (т.е. без ошибок времени выполнения):
      • в сущности это утверждение assert(a == b)
    • Уровень типа: происходит в компиляторе через проверку типов (т.е. без ошибок компилятора):
      • по сути это сравнение типов: например implicitly[A =:= B]
      • A <:< B, компилируется только если A это подтип B
      • A =:= B, компилируется только если A это подтип B а также B это подтип A
      • A <%< B, ("видимый как") компилируется, только если A просматривается как B (т.е. есть неявное преобразование из A к подтипу B)
      • пример
      • больше операторов сравнения

Преобразование между типами и значениями

  • Во многих примерах типы, определенные с помощью признаков, часто бывают как абстрактными, так и запечатанными, и поэтому не могут быть созданы ни непосредственно, ни через анонимный подкласс. Так что это часто используется null в качестве значения заполнителя при выполнении вычисления уровня значения с использованием некоторого типа интереса:

    • например val x:A = null, где A это тип, который вам небезразличен

  • Из-за стирания типов все параметризованные типы выглядят одинаково. Кроме того, (как упомянуто выше) значения, с которыми вы работаете, имеют тенденцию быть null и, следовательно, обусловливание типа объекта (например, с помощью оператора сопоставления) неэффективно.

Хитрость заключается в использовании неявных функций и значений. Базовый регистр обычно является неявным значением, а рекурсивный регистр обычно является неявной функцией. В самом деле, программирование на уровне типов активно использует последствия.

Рассмотрим этот пример ( взят из metascala и 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]]]

(Это очень похоже на определение 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, что вы хотите проверить, равны. Затем проверьте, что следующая компиляция:

Кроме того, вы можете преобразовать тип в значение (как показано выше) и выполнить проверку значений во время выполнения. Например assert(toInt(a) == toInt(b)), где a имеет тип A а также b имеет тип B,

Дополнительные ресурсы

Полный набор доступных конструкций можно найти в разделе типов справочного руководства по scala (pdf).

У Адриана Мурса есть несколько научных статей о конструкторах типов и связанных темах с примерами из scala:

Apocalisp - это блог со многими примерами программирования на уровне типов в scala.

ScalaZ - очень активный проект, который предоставляет функциональные возможности, расширяющие Scala API с использованием различных функций программирования на уровне типов. Это очень интересный проект, у которого много поклонников.

MetaScala - это библиотека уровня типов для Scala, включающая мета-типы для натуральных чисел, логические значения, единицы измерения, HList и т. Д. Это проект Джеспера Норденберга (его блог).

Michid (блог) имеет несколько замечательных примеров программирования на уровне типов в Scala (из другого ответа):

Debasish Ghosh (блог) также имеет несколько соответствующих сообщений:

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

Источник

В дополнение к другим ссылкам здесь, есть также мои сообщения в блоге о метапрограммировании на уровне типа в Scala:

Источник

Как предложено в Твиттере: Shapeless: исследование универсального / политипического программирования в Scala Майлза Сабина.

Источник
Источник

У Scalaz есть исходный код, вики и примеры.

Источник
Другие вопросы по тегам