Каковы некоторые примеры программирования на уровне типоразмеров?

Ответ 1

В большинстве статически типизированных языков у вас есть два "домена" уровня ценности и уровня типа (на некоторых языках есть еще больше). Типовое программирование включает логику кодирования (часто функцию абстракции) в системе типов, которая оценивается во время компиляции. Некоторыми примерами могут быть метапрограммирование шаблонов или семейства типов Haskell.

Для этого примера в Haskell требуется несколько языковых расширений, но пока вы игнорируете их и просто смотрите на семейство типов как на функцию, а на номера типов типов (Nat).

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

import GHC.TypeLits
import Data.Proxy

-- value-level
odd :: Integer -> Bool
odd 0 = False
odd 1 = True
odd n = odd (n-2)

-- type-level
type family Odd (n :: Nat) :: Bool where
    Odd 0 = False
    Odd 1 = True
    Odd n = Odd (n - 2)

test1 = Proxy :: Proxy (Odd 10)
test2 = Proxy :: Proxy (Odd 11)

Здесь вместо того, чтобы проверять, является ли натуральное число значение нечетным числом, мы проверяем, является ли натуральный тип номера нечетным числом и сводит его к логическому уровню на этапе компиляции. Если вы оцениваете эту программу, типы test1 и test2 вычисляются во время компиляции:

λ: :type test1
test1 :: Proxy 'False
λ: :type test2
test2 :: Proxy 'True

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

Ответ 2

Вы уже знакомы с программированием "уровень ценности", посредством которого вы управляете такими значениями, как 42 :: Int или 'a' :: Char. В таких языках, как Haskell или Scala, программирование на уровне шрифта позволяет вам манипулировать такими типами, как Int :: * или Char :: *, где * - тип конкретного типа (Maybe a или [a] - это конкретные типы, но не Maybe или [], которые имеют вид * -> *).

Рассмотрим эту функцию

foo :: Char -> Int
foo x = fromEnum x

Здесь foo принимает значение типа Char и возвращает новое значение типа Int с помощью экземпляра Enum для Char. Эта функция управляет значениями.

Теперь сравните foo с этим типом семейства, включенным с расширением языка TypeFamilies.

type family Foo (x :: *)
type instance Foo Char = Int

Здесь foo принимает тип вида * и возвращает новый тип вида *, используя простое сопоставление Char -> Int. Это функция уровня типа, которая управляет типами.

Это очень простой пример, и вы можете подумать, как это может быть полезно. Используя более мощные языковые инструменты, мы можем начать кодировать доказательства правильности нашего кода на уровне типа (подробнее об этом см. Curry-Howard соответствие).

Практическим примером является красно-черное дерево, использующее программирование уровня, чтобы статически гарантировать сохранение инвариантов дерева.

Красно-черное дерево имеет следующие простые свойства:

• A node либо красный, либо черный.
• Корень черный.
• Все листья черные. (Все листья имеют тот же цвет, что и корень.)
• Каждый красный node должен иметь два черных дочерних узла. каждый путь от данного node к любому из его потомков-потомков содержит такое же количество черных узлов.

Мы будем использовать DataKinds и GADTs, очень мощную комбинацию программирования уровня.

{-# LANGUAGE DataKinds, GADTS, KindSignatures #-}

import GHC.TypeLits

Во-первых, некоторые типы для представления цветов.

data Colour = Red | Black -- promoted to types via DataKinds

это определяет новый вид Colour, населенный двумя типами: Red и Black. Обратите внимание, что нет значений (игнорирующих доны), обитающих в этих типах, но мы их не будем им в любом случае.

Узлы красно-черного дерева представлены следующим GADT

-- 'c' is the Colour of the node, either Red or Black
-- 'n' is the number of black child nodes, a type level Natural number
-- 'a' is the type of the values this node contains
data Node (c :: Colour) (n :: Nat) a where
    -- all leaves are black
    Leaf :: Node Black 1 a
    -- black nodes can have children of either colour
    B    :: Node l     n a -> a -> Node r     n a -> Node Black (n + 1) a
    -- red nodes can only have black children
    R    :: Node Black n a -> a -> Node Black n a -> Node Red n a

GADT позволяет выразить Colour конструкторов R и B непосредственно в типах.

Корень дерева выглядит следующим образом:

data RedBlackTree a where
    RBTree :: Node Black n a -> RedBlackTree a

Теперь невозможно создать хорошо типизированный RedBlackTree, который нарушает любое из 4 упомянутых выше свойств.

• Первое ограничение, очевидно, верно, существует только 2 типа, населяющих Colour.
• Из определения RedBlackTree корень черный.
• Из определения конструктора Leaf все листья черные.
• Из определения конструктора R, как он должен be Black узлы. Кроме того, число черных дочерних узлов каждого поддерева равно (тот же n используется в типе левого и правого поддеревьев)

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

Ответ 3

Другие ответы очень приятные, но я хочу подчеркнуть один момент. Наша теория языков терминов основывается на исчислении Лямбды. "Чистый" Lisp соответствует (более или менее) сильно затушеванному нетипизированному лямбда-исчислению. Смысл программ определяется правилами оценки, которые говорят о том, как термины исчисления лямбда сокращаются по мере запуска программы.

На типизированном языке мы присваиваем типы терминам. Для каждого правила оценки у нас есть соответствующее правило типа, которое показывает, как типы сохраняются при оценке. В зависимости от системы типов существуют также другие правила, определяющие, как типы относятся друг к другу. Оказывается, когда вы получаете достаточно интересную систему типов, типы и их система правил также соответствуют варианту лямбда-исчисления!

Хотя обычно думать о Lambda Calculus как о языке программирования сейчас, он изначально был разработан как система логики. Вот почему это полезно для рассуждения о типах терминов на языке программирования. Но аспект языка программирования Lambda Calculus позволяет писать программы, которые оцениваются с помощью проверки типа.

Надеюсь, теперь вы можете видеть, что "программирование на уровне типоразмеров" не является существенно иной, чем "программирование на уровне термина", это просто то, что сейчас не очень часто существует язык в системе типов, достаточно мощный, чтобы вы У меня есть причина писать в нее программы.