Типичные экземпляры на основе предикатов типа?

Question

Чтобы создать класс типа, который принимает натуралов на уровне типа Z, (SZ), (S (SZ)) ... и т.д., вы можете просто объявить экземпляры рекурсивно как таковой:

data Z 
data S a 

class Type a 

instance Type Z 
instance Type (S a) 

Является ли это возможно создать экземпляр класса типа на основе предикатов уровня уровня? Например, я хочу, чтобы иметь возможность сказать:

{-# LANGUAGE MultiParamTypeClasses #-} 
class Type a b 
instance Type x y when (x :+: y == 8) 

Где :+: является добавление уровня типа и == является уровень типа равенства из Data.Type.Equality, так что экземпляры создаются только для пар нац, которые добавляют до 8 .

Обозначения, подобные этому, доступны в Haskell? Если нет, как это сделать?

Edit: Этот пост был вдохновлен by the Haskell wiki article on smart constructors, где тип класса InBounds был объявлен статически проверить, что тип фантом аргумент, передаваемый в смарт-конструктор был в некотором диапазоне Nat с, умный конструктор был:

resistor :: InBounds size => size -> Resistor size 
resistor _ = Resistor 

Попытки сделать что-то подобное в моем примере (после использования ответа leftaroundabout в) дает мне ошибку:

construct :: (Type a b) => a -> b -> MyType a b 
construct _ _ = MyType 

>>> Expected a type, but a has kind Nat… 

пример из вики Haskell работает, потому что Безразлично» t использовать DataKinds, можно ли передать тип вида Nat функции уровня ценности?

Answer 1

Вам необходимо использовать не предикат равенства, а равенство ограничение (которое испечено на языке, разрешено с помощью -XGADTs).

{-# LANGUAGE KindSignatures, DataKinds, MultiParamTypeClasses, FlexibleInstances, GADTs #-} 

import GHC.TypeLits 

class Type (a :: Nat) (b :: Nat) 

instance (a + b) ~ 8 => Type a b 

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

Answer 2

Вы могли бы написать функцию уровня типа

type family NatEq (a :: Nat) (b :: Nat) :: Bool 
type instance NatEq 0 0 = True 
... 

А потом

instance Type' (NatEq (a + b) 8) a b => Type a b 
class Type' (x :: Bool) (a :: Nat) (b :: Nat) where ... 
instance Type' True a b where ... 
-- If you wanted a different behaviour otherwise: 
-- instance Type' False a b where ... 

Вам необходимо включить кучу расширений, конечно.

Это работает хорошо, если a и b являются константами, так что a+b может быть сведен к 8 (или другой константе). Если они не являются константами, не ожидайте, что GHC докажет вам уравнение. То есть (используя Int вместо Nat), не ожидайте решения Type x (8-x).