Ограничение типа в объявлении типа
Известный пример типового уровня натуральных чисел:
data Zero
data Succ n
У меня вопрос о желательном ограничении при применении конструктора типов Succ. Например, если мы хотим сделать такое ограничение в определении функции, мы можем использовать класс и контекст, как в этом коде:
class Nat n where
toInt :: n -> Int
instance Nat Zero where
toInt _ = 0
instance (Nat n) => Nat (Succ n) where
toInt _ = 1 + toInt (undefined :: n)
Невозможно использовать toInt (undefined :: Succ Int), все в порядке.
Но как реализовать аналогичные ограничения на конструкции уровня типов (возможно, с некоторыми расширенными расширениями типов)?
Например, я бы хотел разрешить использование конструктора типа Succ только с типом Zero и с чем-то вроде этого: Succ (Succ Zero), Succ (Succ (Succ Zero)) и так далее.
Как избежать такого плохого примера во время компиляции:
type Test = Succ Int
(на данный момент нет ошибки компиляции)
P.S.: Мне интереснее как создать ограничение на объявление типа последнего образца
Ответы 1
В настоящее время мы используем расширение DataKinds:
{-# LANGUAGE DataKinds, KindSignatures, ScopedTypeVariables #-}
-- N is a type, but is also a kind now
-- Zero, Succ Zero, ... are values, but are also type-level values of
-- kind N
data N = Zero | Succ N
-- (We could import Proxy the library, instead)
data Proxy (n :: N) = Proxy
-- Now n is restricted to kind N
class Nat (n :: N) where
toInt :: proxy n -> Int
instance Nat Zero where
toInt _ = 0
instance (Nat n) => Nat (Succ n) where
toInt _ = 1 + toInt (undefined :: Proxy n)
Затем мы можем использовать toInt (Proxy :: Proxy (Succ Zero)). Вместо этого toInt (Proxy :: Proxy (Succ Int)) выдаст вид ошибки, как и хотелось.
Лично я бы также заменил прокси на более современные вещи, такие как AllowAmbiguousTypes и TypeApplications, чтобы удалить неиспользуемый аргумент.
{-# LANGUAGE DataKinds, KindSignatures, ScopedTypeVariables,
AllowAmbiguousTypes, TypeApplications #-}
data N = Zero | Succ N
-- Now n is restricted to kind N
class Nat (n :: N) where
toInt :: Int
instance Nat Zero where
toInt = 0
instance (Nat n) => Nat (Succ n) where
toInt = 1 + toInt @n
Используйте это как toInt @(Succ Zero). Синтаксис toInt @n выбирает n в классе типов. Он не соответствует никакому значению, обмениваемому во время выполнения, а только аргументу уровня типа, существующему во время компиляции.
С использованием
type Foo = Succ Int
также ошибки, как хотелось:
• Expected kind ‘N’, but ‘Int’ has kind ‘*’
• In the first argument of ‘Succ’, namely ‘Int’
In the type ‘Succ Int’
In the type declaration for ‘Foo’
Спасибо; только что заметил еще один: Proxy в class Nat (n :: N) where toInt :: proxy n -> Int...
@WillNess Нет, на самом деле это стандартная идиома (которая мне не нравится, но я соглашусь). Использование переменной типа proxy вместо типа Proxy позволяет использовать и другие типы прокси. Часто используется в библиотеки
@chi, я запутался, но твой первый пример не компилируется. Второй неправильный: во-первых, вы немного изменили условие. Succ не является конструктором значений, как вы написали, но должен быть конструктором типа. И настоящая ошибка 2-го примера >:3:12: error: Not in scope: type constructor or class 'Succ'A data constructor of that name is in scope; did you mean DataKinds?
Я имею в виду для 2-го образца: Main> type Foo = Succ Int<interactive>:3:12: error:Not in scope: type constructor or class 'Succ'A data constructor of that name is in scope; did you mean DataKinds?
@Vladimir Вы не скопировали весь мой код на Haskell, включая строку, которая включает DataKinds
Я скопировал 1-й ваш образец и получил: C:_TMP\Haskell\tmp>ghci ans1.hs GHCi, версия 8.6.5: [1 из 1] Компиляция Main (ans1.hs, интерпретируется) ans1.hs:18: 37: ошибка: * Ожидается тип, но n' has kind N' * В сигнатуре типа выражения: n В первом аргументе toInt', namely (undefined :: n)' Во втором аргументе (+)', namely toInt (undefined :: n)' | 18 | toInt _ = 1 + toInt (не определено :: n) | ^ Ошибка, модули не загружены.
Второй пример работает так, как вы описали, если я поместил type Foo = Succ Int в файл кода (а не в ghci, как раньше). Но роль Succ в вашем коде мне пока не ясна :(
@ Владимир, я действительно забыл (undefined :: Proxy n) в своем первом фрагменте, извините. Это должно быть исправлено сейчас. О Succ: играет ту же роль, что и в вашем вопросе. Succ Int — это ошибка, так как Succ хочет число в N, а не тип — это то, что вы хотели, верно? Таким образом, вы можете использовать только Succ Zero, Succ (Succ Zero), ....
В моем коде (условиях, если хотите) Succ является конструктором типов, но в вашем коде Succ выглядит как конструктор данных (значений). Меня это смущает... Возможно, это форма DataKinds магии?
@Vladimir Да, это DataKinds в действии. С этим расширением конструкторы уровня терминов, такие как Zero, Succ в моем коде, «поднимаются» на уровне типа. Таким образом, вы можете использовать их как обычно в значениях, но вы также можете использовать их в типах. Обозначение class Nat (n : N) указывает, что Nat — это не класс типов (мы не можем использовать Nat Bool), а класс N (мы можем использовать Nat Zero), поэтому он относится к поднятым значениям. Итак, у нас есть Int, Maybe Int, [Int] :: * как простые типы и Zero, Succ Zero, ... :: N как «числа на уровне типа». Здесь * и N называются «видами» (своего рода «тип типа»).
См. Что такое расширение DataKinds для Haskell? именно этот пример.