聲明參數化類型同義詞的實例

Question

我有一堆可以在Vectors上工作的函數，即具有強制類型長度的列表。

我試圖讓我的類型更容易編寫，即而不是寫

foo :: (Fold Integer v, Map Integer Integer v v, ...) => ... 

我聲明瞭一個新的類NList這樣我就可以寫foo :: NList v Integer => ...

（簡化）班看起來是這樣的：

class (Fold (v i) i 
     , Map i i (v i) (v i) 
     , Map i (Maybe i) (v i) (v (Maybe i)) 
    ) => NList v i 

正如你所看到的，我必須保持「載體」類型從「項目」分離式（即v與i分開），這樣我就可以將Map這樣的東西寫到Maybe載體上。

因此，v必須有種類* -> *和i種類*。

然而，當我嘗試用向量初始化它，像這樣：

instance NList Vec2 Integer 
instance NList Vec3 Integer 
... 

我得到以下錯誤：

Type synonym `Vec2' should have 1 argument, but has been given none 
In the instance declaration for `NList Vec2 Integer' 

現在，我很新的輸入級編程，我知道我很可能以非常落後的方式來做這件事。是否有可能像這樣實例化一個類型的同義詞？是否有任何類型嚮導有更好的方法來實現我的目標的建議？

Answer 1

這裏的問題是，Vec2和Vec3大概是聲明是這樣的：

type Vec2 a = Vec (S (S Z)) a 
type Vec3 a = Vec (S (S (S Z))) a 

類型同義詞不能被部分應用，各種神祕的原因，（他們會導致類型級lambda表達式，這破壞與各種與實例解析和推理有關的事情 - 試想一下，如果你可以定義type Id a = a並使其成爲Monad的實例）。

也就是說，你不能讓Vec2成爲任何事物的實例，因爲你不能使用Vec2就好像它是一個類型爲* -> *的完全類型構造函數;它實際上是一個只能被完全應用的類型級「宏」。

但是，您可以定義同義詞類型爲部分應用程序本身：

type Vec2 = Vec (S (S Z)) 
type Vec3 = Vec (S (S (S Z))) 

這些都是等價的，不過你的情況下，將被允許。

如果您Vec3類型實際上看起來像

type Vec3 a = Cons a (Cons a (Cons a Nil))) 

或類似的，那麼你的運氣了;如果您想提供任何實例，則必須使用newtype包裝。（在另一方面，你應該能夠避免直接在這些類型的定義情況下完全通過給實例爲Nil和Cons代替，讓您使用Vec3爲一個實例。）

注意與GHC 7.4的新constraint kinds，你能避免單獨的類型完全，並簡單地定義一個約束同義詞：

type NList v i = 
    (Fold (v i) i 
    , Map i i (v i) (v i) 
    , Map i (Maybe i) (v i) (v (Maybe i)) 
    ) 

至於在一般無二，它應該基本上做工精細你的方法; 包使用了相同的總體思路。大量的類和大的上下文可能會使錯誤消息非常混亂並且減慢編譯速度，但這就是類型級hackery的本質。但是，如果你有定義爲通常GADT基地Vec類型：

data Vec n a where 
    Nil :: Vec Z a 
    Succ :: a -> Vec n a -> Vec (S n) a 

，那麼你實際上並不需要任何類型類的。如果在一些其他方式的已定義，但仍parametrised在類型級的自然，那麼你就可以更換所有類：

data Proxy s = Proxy 

class Nat n where 
    natElim 
     :: ((n ~ Z) => r) 
     -> (forall m. (n ~ S m, Nat m) => Proxy m -> r) 
     -> Proxy n 
     -> r 

這應該讓你完全消除背景，但使得定義操作對向量有點棘手。