haskell - 在签名中约束构造函数

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，但我担心这是一个兔子洞。永远无法真正让他们做我想做的事。有谁知道我如何只将 WTrans 参数强制执行到 ofTheAbyss 中？或者我只是完全错过了一些东西。

谢谢。

最好的，
埃里克

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作为 GHC 反对存在主义 newtype s。

您现在可以自由地写 Sort - 通用操作。如果你有通用输入，你可以只使用多态性，有效地柯里化(Currying) Some p -> ...如 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 需要存在-通用输出:在这里我将它用于输入和输出。

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))

因此，使用嵌入式类型系统并不可怕。有时是有代价的:如果你想让你的嵌入式语言有子排序，你可能会发现你做额外的计算只是为了改变某些数据类型的索引，而对数据本身没有影响。如果您不需要子排序，那么额外的纪律通常可以成为真正的 friend 。