我如何向GHC证明(b ~ Foo)？

Question

新问题

我不会假装我知道如何思考或谈论haskell。在伪java-oo-行话中：

我想做的是有一个“结构”来“实现”一个“接口”。该接口的一部分是一个函数，它返回一个实现另一个接口的对象。

interface IFiz {}

interface IBuz {
    function IFiz getFiz() 
}

class Foo implements IFiz { ... }
class Bar implements IBuz {
    IFiz fiz = new Foo();
    function getFiz() {
        return fiz;
    }
}

我如何在Haskell中做到这一点？下面描述了我这样做的尝试。

老问题

我如何向GHC证明(b ~ Foo)？

我对这个问题的理解是：

Foo是类型类Fiz的一个实例。

我希望Bar成为类型类Buz的一个实例。

但是，编译器无法在punk方法的实现中推导出(b ~ Foo)。但它还能是什么呢？我尝试使用废弃的直接方法添加数据约束，也尝试使用GADT，但这两种方法似乎都不起作用(我仍然得到完全相同的错误)。

data Foo = Foo Int                                                                                                                                                                                                                           
data Bar = Bar Foo                                                                                                                                                                                                                           
                                                                                                                                                                                                                                           
class Fiz a where                                                                                                                                                                                                                            
    funk :: a -> a -- Not important, I just wanted to put something in Fiz                                                                                                                                                                                                                           
                                                                                                                                                                                                                                           
class Buz a where                                                                                                                                                                                                                            
    punk :: Fiz b => a -> b                                                                                                                                                                                                                  
                                                                                                                                                                                                                                           
instance Fiz Foo where                                                                                                                                                                                                                       
    funk a = a                                                                                                                                                                                                                               
                                                                                                                                                                                                                                           
instance Buz Bar where                                                                                                                                                                                                                       
   punk (Bar foo) = foo

Could not deduce (b ~ Foo)
from the context (Fiz b)
  bound by the type signature for punk :: Fiz b => Bar -> b
  at Test.hs:42:5-8
  ‘b’ is a rigid type variable bound by
      the type signature for punk :: Fiz b => Bar -> b at Test.hs:42:5
Relevant bindings include punk :: Bar -> b (bound at Test.hs:42:5)
In the expression: foo
In an equation for ‘punk’: punk (Bar foo) = foo

Answer 1

此类型签名：

class Buz a where
  punk :: Fiz b => a -> b

表示如果punk是b的实例，则它必须能够为任何类型的b返回类型为Fiz的内容。所以问题不是编译器不能推断出Foo是Fiz的实例，而是返回值不是Quux，而是Fiz的实例。

data Quux = Quux 

instance Fiz Quux where
  funk a = a

如果您想让带函数类型类返回任何Fiz实例，您可以使用ExistentionalQuantification扩展：

{-# LANGUAGE RankNTypes, ExistentialQuantification #-}   
data Foo = Foo Int
data Bar = Bar Foo
data SomeFiz = forall a . Fiz a => SomeFiz a
class Fiz a where
  funk :: a -> a

class Buz a where
  punk :: a -> SomeFiz

instance Fiz Foo where
  funk a = a

instance Buz Bar where
  punk (Bar foo) = SomeFiz foo

否则，如果您真的想实现此类型类，则只能通过将底层传递给funk来实现

instance Buz Bar where
  punk _ = funk undefined
-- or for example:
instance Buz Bar where
  punk _ = funk (funk undefined)

或者通过修复funk：

instance Buz Bar where
  punk _ = fix funk

如果你能给出你想要实现的更多细节，也许我能给出更有帮助的答案。

Answer 2

你不能这么做。

类Buz表示，如果a有一个Buz实例，那么对于每个有b实例的b，您可以从a -> b中提供一个函数。Fiz类实际上在生成b方面没有提供任何帮助；funk只有在您已经拥有b的情况下才会提供b。

您可能误解了来自GHC的错误消息。类型推断是双向的。在本例中，b来自类Buz中的punk签名。它要求对于每个类型b，punk的结果都是某种类型的b。Foo并不是所有类型的东西。

  ‘b’ is a rigid type variable bound by
      the type signature for punk :: Fiz b => Bar -> b at Test.hs:42:5