Средства для генерации типов Haskell в Haskell («Haskell второго порядка»)?

Question

Заранее извиняюсь, если этот вопрос немного расплывчатый.Это результат мечтательных выходных.

С замечательной системой типов Haskell приятно представить математическую (особенно алгебраическую) структуру в виде классов типов.Я имею в виду, просто посмотрите на числовой прелюдии !Но использование такой замечательной структуры типов на практике всегда казалось мне трудным.

У вас есть хороший способ системы типов выразить, что v1 и v2 являются элементами векторного пространства V, а w является элементом векторного пространства W,Система типов позволяет написать программу с добавлением v1 и v2, но не v1 и w.Большой!Но на практике вам, возможно, захочется поиграть с потенциально сотнями векторных пространств, и вы определенно не хотите создавать типы V1, V2, ..., V100 и объявлять их экземплярами класса типов векторного пространства!Или, может быть, вы читаете некоторые данные из реального мира, в результате чего появляются символы a, b и c - вы можете захотеть выразить, что свободное векторное пространство над этими символами действительно является векторным пространством!

Так ты застрял, верно?Чтобы сделать многие вещи, которые вы хотели бы сделать с векторными пространствами в научной вычислительной среде, вы должны отказаться от своей системы типов, отказавшись от класса типов векторных пространств, и вместо этого функции должны выполнять проверки совместимости во время выполнения.Должны ли вы?Разве нельзя использовать тот факт, что Haskell является чисто функциональным, чтобы написать программу, которая генерирует все нужные вам типы и вставляет их в настоящую программу?Существует ли такая техника?Обязательно укажите, если я просто пропускаю что-то простое здесь (я, вероятно, так): -)

Редактировать: Только сейчас я обнаружил fundeps .Я должен немного подумать о том, как они относятся к моему вопросу (просвещающие комментарии по этому поводу приветствуются).

Answer 1

Шаблон Haskell позволяет это. вики-страница имеет несколько полезных ссылок;в частности учебники Булата .

Синтаксис объявления верхнего уровня - это тот, который вам нужен.Набрав:

mkFoo = [d| data Foo = Foo Int |]

, вы создадите соединение Template Haskell (например, функцию времени компиляции), которое создаст объявление для data Foo = Foo Int, просто вставив строку $(mkFoo).

Хотя этот небольшой пример не слишком полезен, вы можете предоставить mkFoo аргумент, чтобы контролировать, сколько разных объявлений вы хотите.Теперь $(mkFoo 100) создаст для вас 100 новых объявлений данных.Вы также можете использовать TH для генерации экземпляров классов типов.Мой пакет adaptive-tuple - это очень маленький проект, который использует Template Haskell для выполнения чего-то подобного.

Альтернативным подходом было бы использование Derive , которое автоматически получитэкземпляры класса type.Это может быть проще, если вам нужны только экземпляры.

Answer 2

Также в Haskell есть несколько простых методов программирования на уровне типов. Вот канонический пример:

-- A family of types for the natural numbers
data Zero
data Succ n

-- A family of vectors parameterized over the naturals (using GADTs extension)
data Vector :: * -> * -> * where
    -- empty is a vector with length zero
    Empty :: Vector Zero a
    -- given a vector of length n and an a, produce a vector of length n+1
    Cons  :: a -> Vector n a -> Vector (Succ n) a

-- A type-level adder for natural numbers (using TypeFamilies extension)
type family Plus n m :: *
type instance Plus Zero n = n
type instance Plus (Succ m) n = Succ (Plus m n)

-- Typesafe concatenation of vectors:
concatV :: Vector n a -> Vector m a -> Vector (Plus n m) a
concatV Empty ys = ys
concatV (Cons x xs) ys = Cons x (concatV xs ys)

Найдите минутку, чтобы принять это. Я думаю, что это довольно волшебно, что это работает.

Тем не менее, программирование на уровне типов в Haskell находится в feature-uncanny-valley - достаточно, чтобы привлечь внимание к тому, сколько вы не можете сделать. Языки с независимой типизацией, такие как Agda , Coq и Epigram , используют этот стиль до предела и на полную мощность.

Шаблон Haskell во многом похож на обычный стиль генерации кода в LISP-макросах. Вы пишете код для написания кода, а затем говорите: «Хорошо, вставьте этот сгенерированный код сюда». В отличие от описанного выше метода, вы можете написать любой вычислимый код таким способом, но вы не получите очень общую проверку типов, как показано в concatV выше.

Итак, у вас есть несколько вариантов сделать то, что вы хотите. Я думаю, что метапрограммирование - действительно интересное пространство, и в некоторых отношениях оно еще довольно молодо. Веселитесь, исследуя. : -)