Тип Деконструкция

Question

Моих типов данных всегда будут иметь по крайней мере два параметра, а последние два параметра всегда «д» и «т», соответственно:

{-# LANGUAGE TypeFamilies, FlexibleContexts, UndecidableInstances, TypeOperators, DataKinds, ConstraintKinds, FlexibleInstances #-} 

data D1 q m = D1 q 
data D2 t q m = D2 q 

class Foo a where -- a has kind * -> * 
    f :: a x -> a x 

class (Foo b) => Bar b where -- b has kind * -> * 
    -- the purpose of g is to change ONE type parameter, while fixing the rest 
    -- the intent of the equality constraints is to decompose the parameter b into 
    -- its base type and 'q' parameter, then use the same base type with a *different* 
    -- `q` parameter for the answer 
    g :: (b ~ bBase q1, b' ~ bBase q2) => b m -> b' m 

instance (Foo (D2 t q), Integral q) => Bar (D2 t q) where 
    g (D2 q) = D2 $ fromIntegral q -- LINE 1 

результаты этой программы в ошибке

Could not deduce (bBase ~ D2 t0) (LINE 1) 

Когда я написал экземпляр, я, конечно, намеревался указать bBase ~ D2 t. Я думаю, что t не связано каким-то образом (следовательно, введение t0), и я не знаю, может ли GHC деконструировать этот тип вообще. Или, может быть, я просто делаю что-то глупое.

Более того, этот тип разложения типа/декомпозиции типа не требовался бы, если я делаю параметр для Bar имеющим вид * -> * -> *. Но тогда я не мог принудить Foo ограничение:

class (Foo (b q)) => Bar b where -- b has kind * -> * -> * 
    g :: b q m -> q b' -- this signature is now quite simple, and I would have no problem implementing it 

Это не будет работать, потому что д не является параметром для бара, и я не хочу его параметра Bar.

Я нашел решение, используя два дополнительных «пустышку» связанные типы, но я действительно не нравится иметь их вокруг, если я не нуждаюсь в них:

class (Foo b, b ~ (BBase b) (BMod b)) => Bar b where -- b has kind * -> * 
    type BBase b :: * -> * -> * 
    type BMod b :: * 

    g :: (Qux (BMod b), Qux q') => b m -> (BBase b) q' m 

instance (Foo (D2 t q), Integral q) => Bar (D2 t q) where 
    type BBase (D2 t q) = D2 t 
    type BMod (D2 t q) = q 

    g (D2 q) = D2 $ fromIntegral q 

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

Я ищу решение для любого подхода: либо скажите мне, как я могу принудить ограничение класса к «более прикладному» типу, либо расскажу, как сделать типы GHC-деконструирования.

Спасибо!

Answer 1

Из того, что вы описали, у вас есть типы b' :: * -> * -> *, для которых вы хотите ограничить применение b' t :: * -> * (для всех t).

Как summise, вам необходимо либо деконструкции типа, который ваша попытка здесь начиная с b :: * -> * предполагается результат типа приложения b = b' t или приведение в исполнение ограничения на «более-прикладному» тип, а не с начальной точки b' :: * -> * -> *.

Деконструкция типа невозможна, поскольку компилятор не знает, является ли «b» «деконструируемым». Действительно, это может быть не так, например, я могу сделать экземпляр instance Bar Maybe, но Maybe не может быть деконструирован в тип b' :: * -> * -> * и некоторый тип t :: *.

Начиная вместо от типа b' :: * -> * -> *, ограничения на применении b' может быть перемещен в тело класса, где количественно переменные:

class Bar (b :: * -> * -> *) where 
     g :: (Foo (b q1), Foo (b q2)) => b q1 m -> b q2 m 

Для примера есть еще одна морщина: q1 и q2 могут иметь свои собственные ограничения, например для экземпляра D2 вам требуется ограничение Integral. Тем не менее, Bar исправляет ограничения на q1 и q2 для всех экземпляров (в данном случае пустого ограничения).Решение состоит в том, чтобы использовать «ограничительный kinded семьи типа», которые позволяют экземплярам определить свои собственные ограничения:

class Bar (b :: * -> * -> *) where 
     type Constr b t :: Constraint 
     g :: (Foo (b q1), Foo (b q2), Constr b q1, Constr b q2) => b q1 m -> b q2 m 

(включая {-# LANGUAGE ConstraintKinds #-} и импорт GHC.Prim)

Тогда вы можете написать D2 экземпляр:

instance Bar (D2 t) where 
     type Constr (D2 t) q = Integral q 
     g (D2 q) = D2 $ fromIntegral q