我目前正在学习Haskell的类型系统,但是我在类型族和类示例方面遇到了一些麻烦。
下面是我的代码:
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
module Test() where
import Data.Kind (Type)
data Color = ColorWhite | ColorBlack
type Board :: Color -> Type
data Board c where
MkBoard :: (PrintableType c) => Board c
type ExBoard :: Type
data ExBoard where
MkExBoard :: Board t -> ExBoard
type NextColor :: Color -> Color
type family NextColor c where
NextColor 'ColorWhite = 'ColorBlack
NextColor 'ColorBlack = 'ColorWhite
class PrintableType a where
printT :: String
instance PrintableType 'ColorWhite where
printT = "White"
instance PrintableType 'ColorBlack where
printT = "Black"
withBoard :: ExBoard -> (forall c. Board c -> a) -> a
withBoard (MkExBoard b) f = f b
printInfo :: ExBoard -> String
printInfo eb = withBoard eb $ \b@MkBoard -> printTurn b
printTurn :: forall c. PrintableType c => Board c -> String
printTurn _ = printT @c ++ " turn!"
compute :: Board c -> Board (NextColor c)
compute _ = MkBoard
-- >>> printInfo $ MkExBoard $ MkBoard @'ColorWhite
-- >>> printInfo $ MkExBoard $ MkBoard @'ColorBlack
-- "White turn!"
-- "Black turn!"
现在,compute
函数给我的错误是"No instance for (PrintableType (NextColor c)) arising from a use of ‘MkBoard’"
,这让我很困惑,因为NextColor c
的两个输出都已经定义为PrintableType
的示例。
如果我从MkBoard
中删除了(PrintableType c)
,那么printTurn
开始给我错误No instance for (PrintableType c) arising from a use of ‘printTurn’
,而compute
不再给予我错误。
考虑到这一点,我只能猜测编译器没有解析类型族结果的类示例。有没有什么方法可以让我在MkBoard
中保留(PrintableType c)
,因为print函数,并且还可以解决compute
函数的问题?或者我在这里遗漏了什么?
2条答案
按热度按时间5cnsuln71#
GHC没有一种机制来推导整个类型族的约束(例如,
NextColor
的整个映像)。在这个特定的例子中,这将是一个通过少数可能的情况穷举的问题,但通常这是不可能的,并且可能浪费大量的编译时间来尝试。您可以新增类别,以手动执行校样:
您可以通过创建它来保存一些样板文件
但我不认为它会终止,而且不可判定的超类有点不稳定。
liwlm1x92#
我发现--作为一般规则--如果GHC不能推导出一个示例,拍拍它的头,向它保证示例在那里通常是有效的。
在本例中,关键是将GHC所需的确切约束添加到
compute
的类型签名中:在一般情况下,GHC可能会抱怨缺少更多的示例,而您可以继续添加它们,直到程序进行类型检查,或者您开始怀疑您犯了一个可怕的设计错误,需要重新考虑您的方法。