使用幻像类型时避免冗余约束

Question

这是我正在尝试编写代码的一个简化的,也许是愚蠢的例子(这更复杂,涉及列表长度的编译时编码).

鉴于以下内容:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GADTs #-}

data D (a :: Bool) where
  D :: Bool -> D a

我想要以下功能g:

g :: D a -> Bool
g (D x) = x == a

当然,这不会编译为a类型,而不是值.

这是一个可能的解决方案:

class C (a :: Bool) where
  f :: D a -> Bool

instance C True where
  f (D x) = x == True

instance C False where
  f (D x) = x == False

g :: (C a) => D a -> Bool
g = f

但后来我必须添加一个约束g,这似乎是多余的,a :: Bool并且我已经得到了所有情况的实例Bool.

无论如何我可以写g它有签名:

g :: D a -> Bool 

即不需要额外的约束？

Answer 1

不,这是不可能的,因为我可以给你一个非常好的类型值,定义D Any在哪里Any

type family Any :: k where {}

你能做的就是写一个更普遍有用的课程:

data SBool a where
  SFalse :: SBool 'False
  STrue :: SBool 'True

sBoolToBool :: SBool a -> Bool
sBoolToBool SFalse = False
sBoolToBool STrue = True

class KnownBool a where
  knownBool :: SBool a
instance KnownBool 'False where
  knownBool = SFalse
instance KnownBool 'True where
  knownBool = STrue

当然,如果你没有将这些类型用于其他任何事情,那么所有这些机器都是过度的.