约束签名中的构造函数

Question

所以,我正在进行一个有趣的实验,在上下文意义上,我正在碰壁.我正在尝试定义一种数据类型,该数据类型可以是基元,也可以是从一个构造函数转换为另一个构造函数的函数.

data WeaponPart =
    WInt Int |
    WHash (Map.Map String Int) |
    WNull |
    WTrans (WeaponPart -> WeaponPart)

instance Show WeaponPart where
    show (WInt x) = "WInt " ++ (show x)
    show (WHash x) = "WHash " ++ (show x)
    show (WTrans _) = "WTrans"
    show WNull = "WNull"

cold :: WeaponPart -> WeaponPart
cold (WInt x) = WHash (Map.singleton "frost" x)
cold (WHash x) = WHash $ Map.insertWith (+) "frost" 5 x
cold (WTrans x) = cold $ x (WInt 5)
cold (WNull) = cold $ (WInt 5)

ofTheAbyss :: WeaponPart -> WeaponPart
ofTheAbyss (WTrans x) = x (WTrans x)

问题是签名ofTheAbyss允许任何WeaponPart作为参数,而我只想允许WTrans构造的参数.你可以看到我只为这种情况写了一个模式匹配.

我尝试过使用GADT,但我担心这是一个兔子洞.永远不会让他们做我想做的事.有没有人有任何想法如何只能强制执行TheAbyss中的WTrans参数？或者我只是完全错过了一些东西.

谢谢.

最好的,Erik

Answer 1

你可以用GADT做这件事.从我这里来判断是什么结果是兔子洞,但让我至少显示配方.我正在使用新的PolyKinds扩展程序,但你可以用更少的管理.

首先,确定您需要的类型,并定义这些类型的数据类型.

data Sort = Base | Compound

接下来,定义按其排序索引的数据.这就像构建一个小型语言.

data WeaponPart :: Sort -> * where
  WInt    :: Int ->                                   WeaponPart Base
  WHash   :: Map.Map String Int ->                    WeaponPart Base
  WNull   ::                                          WeaponPart Base
  WTrans  :: (Some WeaponPart -> Some WeaponPart) ->  WeaponPart Compound

您可以通过存在量化来表示"任何类型的数据",如下所示:

data Some p where
  Wit :: p x -> Some p

请注意,这x并没有逃脱,但我们仍然可以检查x"满足" 的"证据" p.注意,Some必须是一个data类型,而不是newtype存在主义newtype的GHC对象.

您现在可以自由编写Sort-generic operations.如果你有通用输入,你可以使用多态,有效地currying Some p -> ...as forall x. p x -> ....

instance Show (WeaponPart x) where
  show (WInt x)    = "WInt " ++ (show x)
  show (WHash x)   = "WHash " ++ (show x)
  show (WTrans _)  = "WTrans"
  show WNull       = "WNull"

Sort-generic输出需要存在性:这里我用它来输入和输出.

cold :: Some WeaponPart -> Some WeaponPart
cold (Wit (WInt x))    = Wit (WHash (Map.singleton "frost" x))
cold (Wit (WHash x))   = Wit (WHash $ Map.insertWith (+) "frost" 5 x)
cold (Wit (WTrans x))  = cold $ x (Wit (WInt 5))
cold (Wit WNull)       = cold $ Wit (WInt 5)

我不得不偶尔添加Wit一下这个地方,但这是同一个程序.

同时,我们现在可以写了

ofTheAbyss :: WeaponPart Compound -> Some WeaponPart
ofTheAbyss (WTrans x) = x (Wit (WTrans x))

因此,使用嵌入式系统并不可怕.有时会产生成本:如果您希望嵌入式语言具有子分类,您可能会发现只是为了更改某些数据类型的索引而进行额外的计算,这对数据本身没有任何影响.如果你不需要再分类,额外的纪律通常可以成为真正的朋友.