代码之家 › 专栏 › 技术社区 › WHITECOLOR

使用GADTS/类型族映射规则

type-families gadt haskell

0

WHITECOLOR · 技术社区 · 1 年前

以下是示例输入和输出类型的简单表示:

   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和Families的解决方案变体,在这里我必须为每个引入额外的标签 输入 和 输出 值:

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

我的第一个问题是:这是实现我想要的(使用GADT/家庭)的唯一方法吗?我不喜欢的是,我需要为 Input/Output 价值观,有可能让它变得不那么简单吗?
我的第二个问题是:更高级的映射逻辑可能吗?假设我希望将输入映射到一个输出列表,该列表需要包含一个/servral值:

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

0 回复 | 直到 1 年前

1

3

leftaroundabout 1 年前

实现目标的最简单方法似乎是这样,这也是我可能在实践中使用的方法:只需实现两个函数

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

然后成功

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

如果使用包含元素的类型作为健全性检查太弱,那么您可以始终添加newtype包装器,这可能是一个好主意。

与您的标签相比,这仍然有一些限制。这种方法能够当然也有道理。这需要一些样板,是的。原则上,您实际上不需要为标签定义新的类型,也可以使用

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检查不变量。类型很好,但它们真正的优势在于它们能够真正帮助找到正确的解决方案并表达意图。当你只想 禁止某些代码 ,类型不是一个非常有效的工具,至少在Haskell中不是。如果你真的需要防水的证明,无论如何这不是正确的语言,请使用Agda/Coq/Idris/Lean。如果你只是OTOH 相当高的概率 QuickCheck可以更轻松地完成任务。

2

3

lsmor 1 年前

我认为对于这种特殊的情况,只使用Output标签就可以了,这大大简化了。方法是“用愿望的输出标签标记每个输入和输出”

data OutputTag = A | B | C

data Input (o :: OutputTag) where 
  I1 :: Int    -> Input A
  I2 :: String -> Input B
  
data Output (o :: OutputTag) where 
  OA :: String -> Output A
  OB :: Bool -> Output B
  OC :: Output C

inputToOutput :: (tag ~ tag') => Input tag -> Output tag'
-- inputToOutput (I1 0) = OC -- Uncomment this line, fails with Couldn't match type â'Câ with â'Aâ
inputToOutput (I1 i) = OA (show i)
inputToOutput (I2 s) = OB (s == "x")

给你 snipet 用于此代码。也许你可以用一些不那么复杂的类型族来扩展功能,但我对这个级别的haskell不太熟悉。我想你可以做一些类似的事情

data OutputTag = A | B | C

data Input (o :: [OutputTag]) where 
  I1 :: Int    -> Input [A,C]
  I2 :: String -> Input B
  
data Output (o :: OutputTag) where 
  OA :: String -> Output A
  OB :: Bool -> Output B
  OC :: Output C

-- Here the type family Elem :: OutputTag -> [OutputTag] -> Bool is somthing you have to
-- define or use a library which defines it. I'm not aware of any, but I bet it exists
inputToOutput :: (Elem tag' tags ~ True) => Input tags -> Output tag'
inputToOutput (I1 i) = OA (show i)
inputToOutput (I2 s) = OB (s == "x")