Tip Yapıçözüm

Question

Benim veri türleri her zaman en az iki parametreye sahip olacak ve son iki parametre sırasıyla 'q' ve 'm' her zaman şunlardır: hatası

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

yılında

{-# 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 

Bu program sonuçları

Örneği yazdığımda, kesinlikle bBase ~ D2 t'u hedefledim. Sanırım bir şekilde bağlı değiliz (bu yüzden t0'ın tanıtımı) ve GHC'nin bu türden hiçbir şeyi çözüp çözemeyeceğini bilmiyorum. Ya da belki sadece aptalca bir şey yapıyorum. > * - -> * Ben parametre tür * sahip Bar yaparsanız noktaya

Daha tip eşitlik bu tür/tip yapısöküm gerekli olmaz. Sonra Foo kısıtı zorlamak olamazdı:

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 

q Bar parametre olmadığından Bu çalışmaz ben Bar parametreye istemiyorum.

Ben ilişkili türleri İKİ ekstra "kukla" kullanarak bir çözüm bulundu, ancak ben bunları gerekmiyorsa etraflarında olan pek hoşlanmadığını: Bu işler

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 

, ancak açıkça tutarındaki Örneğin basit tipine göre gereksiz olması gerektiğini düşündüğüm türün yapısını bozar.

Her iki yaklaşım için de bir çözüm arıyorum: "daha fazla uygulanan" türdeki bir sınıf kısıtlamasını nasıl uygulayabileceğimi veya nasıl GHC deconstruct türlerini nasıl yapacağımı anlat.

Teşekkürler!

Answer 1

Uyguladığınızdan, uygulanmış b' t :: * -> *'u (t için) sınırlamak istediğiniz b' :: * -> * -> * türüne sahipsiniz.

sen summise gibi, bir b :: * -> * başlayarak sizin girişimi burada bir türünü yapısızlaştırmak gerek ya bir tip uygulama b = b' t veya "daha uygulanan" konulu bir kısıtlamayı zorlamak için sonucu olduğu varsayılıryerine b' :: * -> * -> * başlangıç ​​noktasından yazın. b "deconstructable" bile eğer derleyici bilmez beri bir tür Yaramaz

, mümkün değildir. Gerçekten de, bu, örneğin, olmayabilir, bir örneği instance Bar Maybe yapabilir, ama Maybe bir tip b' :: * -> * -> * ve bazı tip t :: * içine yapıbozuma edilemez. daki Örneğin

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

bir başka kırışıklık vardır: bir tür b' :: * -> * -> * yerine başlangıç ​​

, b' bir uygulama kısıtlamaları değişkenler nicelendirilir sınıfı gövde içine hareket ettirilebilir: q1 ve q2'nin kendi kısıtlamaları olabilir, örneğin D2 mesela sen Integral kısıtlamayı gerektirir. Ancak Bar (bu durumda boş kısıt olarak) tüm örneklerini q1 ve q2 üzerindeki kısıtlamaları düzeltir.Sonra yazabilir

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 

(dahil {-# LANGUAGE ConstraintKinds #-} ve GHC.Prim içe)

sizin D2 örneği:

bir çözüm örneklerini kendi kısıtlamaları belirtmek için izin "kısıt-kinded tip ailelerin" kullanmaktır

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