Как создать класс вида в Haskell или специальный полиморфизм на уровне типов с использованием семейств типов

Я изучаю особенности семейства типов Haskell и вычисление уровня типов. Кажется, довольно легко получить параметрический полиморфизм на уровне типа, используя PolyKinds:

{-# LANGUAGE DataKinds, TypeFamilies, KindSignatures, GADTs, TypeOperators, UndecidableInstances, PolyKinds, MultiParamTypeClasses, FlexibleInstances #-}

data NatK = Z | S NatK
data IntK = I NatK NatK

infix 6 +
type family (x :: NatK) + (y :: NatK) :: NatK where
    Z     + y = y
    (S x) + y = S (x + y)

-- here's a parametrically polymorphic (==) at the type-level
-- it also deals specifically with the I type of kind IntK
infix 4 ==
type family (a :: k) == (b :: k) :: Bool where
    (I a1 a2) == (I b1 b2) = (a1 + b2) == (a2 + b1)
    a == a = True
    a == b = False

Я могу делать такие вещи, как :kind! Bool == Bool, :kind! Int == Int или :kind! Z == Z и :kind! (I Z (S Z)) == (I (S Z) (S (S Z))).

Однако я хочу сделать type + ad-hoc полиморфным. Так что он ограничен экземплярами, которые я ему даю. Два экземпляра здесь - это типы вида NatK и типы вида IntK.

Сначала я попытался сделать его параметрически полиморфным:

infix 6 :+
type family (x :: k) :+ (y :: k) :: k where
    Z         :+ y = y
    (S x)     :+ y = S (x :+ y)
    (I x1 x2) :+ (I y1 y2) = I (x1 :+ y1) (x2 :+ y2)

Это работает, как и я :kind! (I (S Z) Z) :+ (I (S Z) Z).

Однако я тоже умею :kind! Bool :+ Bool. И это не имеет никакого смысла, но позволяет использовать его как простой конструктор типов. Я хочу создать семейство типов, которое не допускает таких ошибочных типов.

На данный момент я потерялся. Я пробовал классы типов с параметром type. Но это не сработало.

class NumK (a :: k) (b :: k) where
    type Add a b :: k

instance NumK (Z :: NatK) (b :: NatK) where
    type Add Z b = b

instance NumK (S a :: NatK) (b :: NatK) where
    type Add (S a) b = S (Add a b)

instance NumK (I a1 a2 :: IntK) (I b1 b2 :: IntK) where
    type Add (I a1 a2) (I b1 b2) = I (Add a1 b1) (Add a2 b2)

Это все еще позволяет :kind! Add Bool Bool.

Имеет ли это какое-то отношение к расширению ConstraintKinds, где мне нужно ограничить :+ или Add каким-то «добрым классом»?


types typeclass haskell type-families data-kinds
person CMCDragonkai    schedule 18.03.2016    source источник

Ответы (2)


arrow_upward
8
arrow_downward

Самое простое решение - использовать семейства открытого типа для специальной перегрузки и семейства закрытого типа для реализации:

data NatK = Z | S NatK
data IntK = I NatK NatK

type family Add (x :: k) (y :: k) :: k

type family AddNatK (a :: NatK) (b :: NatK) where
  AddNatK Z b = b
  AddNatK (S a) b = S (AddNatK a b)

type family AddIntK (a :: IntK) (b :: IntK) where
  AddIntK (I a b) (I a' b') = I (AddNatK a a') (AddNatK b b')

type instance Add (a :: NatK) (b :: NatK) = AddNatK a b
type instance Add (a :: IntK) (b :: IntK) = AddIntK a b

Если мы хотим, чтобы несколько методов уровня типа и уровня термина были сгруппированы вместе, мы можем написать классы типа, используя KProxy from _ 3_:

class NumKind (kproxy :: KProxy k) where
  type Add (a :: k) (b :: k) :: k
  -- possibly other methods on type or term level

instance NumKind ('KProxy :: KProxy NatK) where
  type Add a b = AddNatK a b

instance NumKind ('KProxy :: KProxy IntK) where
  type Add a b = AddIntK a b

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

Начиная с GHC 8.0, KProxy становится ненужным, поскольку типы и типы будут обрабатываться точно так же:

{-# LANGUAGE TypeInType #-}

import Data.Kind (Type)

class NumKind (k :: Type) where
  type Add (a :: k) (b :: k) :: k

instance NumKind NatK where
  type Add a b = AddNatK a b

instance NumKind IntK where
  type Add a b = AddIntK a b
person András Kovács    schedule 18.03.2016
comment
Спасибо! Это довольно круто, но не могли бы вы подробнее рассказать, что именно заставляет его работать? То есть почему это работает? И для открытого и закрытого решения, и для решения KProxy, и для решения TypeInType. - person CMCDragonkai; 18.03.2016
comment
О, но я только что протестировал ваше первое решение, и оно все еще позволяет :kind! Add Bool Bool, что приводит к Add Bool Bool :: *. Я надеялся, что это станет ошибкой типа, а не будет принято !? - person CMCDragonkai; 18.03.2016
comment
Также ваше второе решение также позволяет Add Bool Bool. Это не проявляется как ошибка типа. - person CMCDragonkai; 18.03.2016
comment
Это неизбежно. Если у нас есть приложение с хорошо подобранным семейством типов и нет подходящего регистра для аргументов, мы получаем зависшее приложение вместо ошибки шаблона, как во время выполнения. Застрявшее приложение нельзя использовать ни для чего (с помощью эзотерического исключение), поэтому такое поведение безопасно. - person András Kovács; 18.03.2016
comment
Итак, ваше решение по определению одного семейства поликиндинговых закрытых типов также безопасно, оно просто не расширяемо / модульно. - person András Kovács; 18.03.2016
comment
Хорошо, я думаю, такое поведение невозможно / нежелательно? - person CMCDragonkai; 19.03.2016
comment
Это действительная альтернатива текущему поведению, возможно, желательная, но определенно невозможная в настоящее время. - person András Kovács; 19.03.2016
comment
@ AndrásKovács, это не единственное эзотерическое исключение. Тот же пакет constraints также определяет (нулевой) класс, который не может иметь никаких экземпляров, использующих class Any => Bottom where no :: Dict a. Поскольку Any является семейством застрявших типов (используется здесь в виде Constraint!), Нет никакого способа удовлетворить его, и, следовательно, нет никакого способа написать даже поддельный экземпляр Bottom. Я не уверен, почему это важно, если это так, но оно есть. - person dfeuer; 30.03.2016

arrow_upward
1
arrow_downward

(Это должен быть комментарий, но мне нужно больше места)

Я пробовал что-то вроде

class GoodK (Proxy k) => NumK (a :: k) (b :: k) where ...

но я потерпел неудачу. Понятия не имею, достижимо ли то, о чем вы просите.

Наилучшее приближение, которое я получил, - это Add Bool Bool kind-check, но сгенерировать неразрешимое ограничение, так что, если мы когда-нибудь его воспользуемся, мы все равно получим ошибку. Возможно, этого хватит для ваших целей (?).

class Fail a where

instance Fail a => NumK (a :: *) (b :: *) where
    type Add a b = ()
person chi    schedule 18.03.2016