與類型

Question

算術約束類型類的實例基本上，我希望能夠做這樣的事情：

{-# LANGUAGE KindSignatures #-} 
{-# LANGUAGE DataKinds #-} 
{-# LANGUAGE TypeOperators #-} 
{-# LANGUAGE FlexibleInstances #-} 
import GHC.TypeLits 

newtype Foo (a::Nat) (b::Nat) c = Foo {getFoo :: c} 

class Clz a where 

instance Clz (Foo a (2*a) c) where 

即，使的Clz只有當a = 2*bFoo a b實例。

我知道問題出在最後一行的(2*a)表達式上。當我嘗試編譯它時，我得到：

• Illegal type synonym family application in instance: 
    Foo a (2 * a) c 
• In the instance declaration for ‘Clz (Foo a (2 * a) c)’ 

有沒有辦法解決這個問題？我將如何改變語法？我需要更多的語言擴展嗎？我正在使用最新的GHC（8.0.1）。

Answer 1

可以使用一種等價的約束（通過啓用GADTs或類型的家庭）：

instance (b ~ (2 * a)) => Clz (Foo a b c) where 

這對於家庭型工作在本other answer看到的常用技術。這個答案有一點更多的解釋：這個約束並不意味着正好與你想要的版本相同，但可能仍然適用於你的目的。