Ограничение типа в объявлении типа - PullRequest
Новая
       65

Ограничение типа в объявлении типа

3 голосов
/ 26 июня 2019

Есть известный пример натуральных чисел уровня типа: 

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

(на данный момент ошибки компиляции нет)

П.С .: Мне интереснее, как создать ограничение на объявление типа последнего образца

1 Ответ

5 голосов
/ 26 июня 2019

В настоящее время мы используем расширение 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’
...