将Dict转变为约束

cro*_*eea 15 haskell ghc

我有一个类Cyc c r,它具有表单数据的功能c m r,其中m是一个幻像类型.例如,

class Cyc c r where
  cyc :: (Foo m, Foo m') => c m r -> c m' r
Run Code Online (Sandbox Code Playgroud)

我没有做出m类参数的充分理由.出于此示例的目的,主要原因是它减少了对函数的约束数量.在我的实际例子中,对这个界面更迫切的需求是我使用更改和隐藏的幻像类型,所以这个界面让我得到Cyc任何幻像类型的约束.

这个选择的一个缺点是我不能制作Num (c m r)超类约束Cyc.我的意图是c m r应该Num随时随地(Cyc c r, Foo m).目前的解决方案非常烦人:我在课堂上添加了方法Cyc

witNum :: (Foo m) => c m r -> Dict (Num (c m r))
Run Code Online (Sandbox Code Playgroud)

哪种方式完成同样的事情.现在,当我有一个带有泛型Cyc并需要Num (c m r)约束的函数时,我可以写:

foo :: (Cyc c r, Foo m) => c m r -> c m r
foo c = case witNum c of
  Dict -> c*2
Run Code Online (Sandbox Code Playgroud)

在课程中我可以添加一个Num (c m r)约束foo,但我想减少约束的数量,还记得吗?(Cyc c r, Foo m)应该暗示一个Num (c m r)约束(我需要Cyc c rFoo m其他目的),所以我不想也写出Num约束.

在写这个问题的过程中,我发现了一种更好的(?)方法来实现这个目标,但它有其自身的缺点.

模块Foo:

{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, ScopedTypeVariables #-}
module Foo where

import Data.Constraint

class Foo m

class Cyc c r where
  cyc :: (Foo m, Foo m') => c m r -> c m' r  
  witNum :: (Foo m) => c m r -> Dict (Num (c m r))

instance (Foo m, Cyc c r) => Num (c m r) where
  a * b = case witNum a of
            Dict -> a * b
  fromInteger a = case witNum (undefined :: c m r) of
                    Dict -> fromInteger a

-- no Num constraint and no Dict, best of both worlds
foo :: (Foo m, Cyc c r) => c m r -> c m r
foo = (*2)
Run Code Online (Sandbox Code Playgroud)

模块栏:

{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, OverlappingInstances #-}
module Bar where

import Foo
import Data.Constraint

data Bar m r = Bar r deriving (Show)

instance (Num r) => Cyc Bar r where
  witNum _ = Dict

instance (Num r, Foo m) => Num (Bar m r) where
  (Bar a) * (Bar b) = Bar $ a*b
  fromInteger = Bar . fromInteger

instance Foo ()  

bar :: Bar () Int
bar = foo 3
Run Code Online (Sandbox Code Playgroud)

虽然这种方法让我得到了我正在寻找的一切,但它似乎很脆弱.我主要担心的是:

  1. 我对Num模块中的通用实例头很警惕Foo.
  2. 如果导入任何重叠实例Foo,我突然需要IncoherentInstancesNum约束foo将实例选择推迟到运行时.

是否有另一种方法可以避免Dict在需要Num (c m r)避免这些缺点的每个功能中使用?

cro*_*eea 1

经过 6 个月的思考,我终于对上面悬而未决的评论有了答案:添加一个newtype包装器!

我把Cyc班级分成两部分:

class Foo m

class Cyc c where
  cyc :: (Foo m, Foo m') => c m r -> c m' r

class EntailCyc c where
  entailCyc :: Tagged (c m r) ((Foo m, Num r) :- (Num (c m r)))
Run Code Online (Sandbox Code Playgroud)

然后我按上面的方式定义我的Cyc实例:

data Bar m r = ...

instance Cyc Bar where ...

instance (Num r, Foo m) => Num (Bar m r) where ...

instance EntailCyc Bar where
  witNum _ = Dict
Run Code Online (Sandbox Code Playgroud)

然后我定义一个新类型包装器并Cyc为其提供一个通用实例:

newtype W c m r = W (c m r)

instance Cyc (W c m r) where cyc (W a) = W $ cyc a

instance (EntailCyc c, Foo m, Num r) => Num (W c m r) where
  (W a) + (W b) = a + b \\ witness entailCyc a
Run Code Online (Sandbox Code Playgroud)

最后,我将所有使用泛型c m r类型的函数更改为使用W c m r类型:

foo :: (Cyc c, EntailCyc c, Foo m, Num r) => W c m r -> W c m r
foo = (*2)
Run Code Online (Sandbox Code Playgroud)

这里的要点是,foo可能需要许多约束(例如Eq (W c m r),,,Show (W c m r)等等),每个约束都单独需要它们自己的约束。W c m r然而, for EqShow等的通用实例都具有完全相同的约束(EntailCyc c, Foo m, Eq/Show/... a),因此上面的约束foo是我需要编写的唯一约束!