GADTS/类型族的映射规则

Question

这些是示例输入和输出类型的简单表示：

   Input = I1 Int | I2 String

   Output = OA String | OB Bool | OC 

这里的参数只是为了更真实。 :)

我想要一个将

Input

映射到

Output

的函数：

inputToOutput = \case
  I1 val -> OA (show val)
  I2 str -> (OB (str == "x"))

但是这个函数应该根据允许映射进行检查（

I1 -> OB

，

I2 -> OB

），所以我不能这样做：

inputToOutput = \case
  I1 val -> OB True -- allows only OA
  I2 str -> OA str -- allows only OB

我有一个带有 GADT 和家庭的解决方案变体，在这里我必须为每个

Input

和

Output

值引入额外的标签：

-- Input tags
data I_ = I1_ | I2_


data Input (i :: I_) where
  I1 :: Int -> Input 'I1_
  I2 :: String -> Input 'I2_


-- Output tags
data O_ = OA_ | OB_ | OC_


data Output (o :: O_) where
  OA :: String -> Output 'OA_
  OB :: Bool -> Output 'OB_
  OC :: Output 'OC_

-- Input/Output rules for tags
type family I2O (i :: I_) :: O_ where
  I2O 'I1_ = 'OA_
  I2O 'I2_ = 'OB_


inputToOutput :: Input a -> Output (I2O a)
inputToOutput = \case
  I1 val -> OA (show val)
  I2 str -> (OB (str == "x"))

1. 我的第一个问题：这是实现我想要的（使用 GADTs/家庭）的唯一方法吗？我在那里不喜欢的是，我需要为

   Input/Output

   值引入额外的样板标签，是否有可能减少样板方式？

2. 我的第二个问题：更高级的映射逻辑是否可能？假设我希望将输入映射到需要包含一个/多个值的输出列表：

inputToOutput = \case
  I1 val -> [ OA (show val), OC] -- also allows other Output values like OC, but not requires
  I2 str -> [(OB (str == "x"))]

Answer 1

实现目标的最简单方法似乎是这个，这也是我在实践中可能会使用的方法：只需实现两个功能

i1case :: Int -> String
i2case :: String -> Bool

然后制作

inputToOutput = \case
  I1 val -> OA $ i1case val
  I2 str -> OB $ i2case str

如果使用包含元素的类型作为健全性检查太弱，您总是可以添加新类型包装器，无论如何这可能是个好主意。

与您的标签相比，这仍然有一些限制。这种方法 could 当然也很有意义。它需要一些样板，是的。原则上你实际上不需要为标签定义新类型，你也可以只使用

data Input (i :: Symbol) where
  I1 :: Int -> Input "I1"
  I2 :: String -> Input "I2"

等等，但我实际上不会推荐这个。

关于你的第二个问题，

是否有更高级的映射逻辑？假设我希望将输入映射到需要包含一个/多个值的输出列表

– 好吧，与其尝试要求一个列表“包含一个”或多个，您可以简单地要求一个就在那里，然后再加上一个您不关心其类型的输出列表。对于后者，你可以使用一个简单的存在包装器，

data SomeOutput where
  SomeOutput :: Output o -> SomeOutput

然后

inputToOutput :: Input a -> (Output (I2O a), [SomeOutput])
inputToOutput = \case
  I1 val -> (OA (show val), [SomeOutput OC])
  I2 str -> (OB (str == "x"), [])

更复杂的要求，比如“最多三个这个构造函数”，也是可能的，但是表达起来会很痛苦。从一些开始

data ORequirement = AtLeast Nat O_
                  | AtMost Nat O_
                  ...
type ORequirements = [ORequirement]

type family IOReq (i :: I_) :: OREquirements where
  IOReq 'I1_ = '[ 'AtLeast 1 'O1_ ]
  ...

type family ConformsRequirements (rs :: ORequirements)
                                 (os :: [O_])
                                 :: Constraint where
  ...

data CertainOutputs (os :: [O_]) where
  Nil/Cons...

inputToOutput :: ConformsRequirements (IOReq a) os
      => Input a -> CertainOutputs os
inputToOutput = ...

你可能会让它工作，但你需要使用大量的

singletons

才能使其可行。我可能不会打扰，而是用 QuickCheck 来检查不变量。