5

所以，我正在做一个有趣的语境意义实验，但我碰壁了。我正在尝试定义一种数据类型，它可以是原始数据类型，也可以是从一个构造函数转换为另一个构造函数的函数。

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 中？或者我只是完全错过了一些东西。

谢谢。

最好的，埃里克

4

3 回答 3

10

你可以用 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'satisfies' 的 'evidence' p。请注意，它Some必须是一个data类型，而不是newtype作为 GHC 对象的存在性newtypes。

您现在可以自由地编写Sort-generic 操作。如果您有通用输入，则可以只使用多态性，有效地柯里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"

-generic 输出需要存在性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))

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

于 2012-05-27T10:07:16.577 回答
3

这是另一种可能的解决方案：将数据类型一分为二。我使用了与其他答案一致的名称，以便于查看相似之处。

data WeaponPartBase
    = WInt Int
    | WHash (Map.Map String Int)
    | WNull

data WeaponPartCompound = WTrans (WeaponPart -> WeaponPart)
data WeaponPart = Base WeaponPartBase | Compound WeaponPartCompound

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

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

这可以通过为基本事物声明一个类来稍微方便一些：

class Basic a where
    wint :: Int -> a
    whash :: Map.Map String Int -> a
    wnull :: a

class Compounded a where
    wtrans :: (WeaponPart -> WeaponPart) -> a

instance Basic WeaponPartBase where
    wint = WInt
    whash = WHash
    wnull = WNull

instance Basic WeaponPart where
    wint = Base . wint
    whash = Base . whash
    wnull = Base wnull

instance Compounded WeaponPartCompound where
    wtrans = WTrans

instance Compounded WeaponPartCompound where
    wtrans = Compound . wtrans

所以例如coldandofTheAbyss可能看起来像这样：

cold' (Base (WInt x)) = whash (Map.singleton "frost" x)
cold' (Base (WHash x)) = whash $ Map.insertWith (+) "frost" 5 x
cold' (Base WNull) = cold' (wint 5)
cold' (Compound (WTrans x)) = cold' (x (wint 5))

ofTheAbyss' (WTrans x) = x (wtrans x)
于 2012-05-27T15:09:58.770 回答
1

您试图不是通过类型而是通过构造函数来约束您的函数。这不是一件可行的事情。

事实上，这不应该是一件可行的事情——如果你正在编写另一个函数，并且你有一些 unknown WeaponPart，你必须能够将它传递给ofTheAbyss或不传递——这必须进行类型检查。

我能想到的两个选择是：

a) 给出ofTheAbysstype (WeaponPart -> WeaponPart) -> WeaponPart，“解包”构造函数。

b）ofTheAbyss在任何其他构造函数上给出运行时错误。

 ofTheAbyss :: WeaponPart -> WeaponPart
 ofTheAbyss (WTrans x) = x (WTrans x)
 ofTheAbyss _ = error "Illegal argument to ofTheAbyss was not a WTrans"
于 2012-05-27T07:15:47.067 回答