英文:
Mapping rules with GADTS/Type Families
问题
-
这是实现您所需的方式之一(使用GADTs/Families)。在这种方法中,您需要为
Input/Output
值引入额外的标签,这可能会导致一些样板代码。是否有可能以更少的样板代码方式实现这一目标,取决于您的具体需求和编程语言的支持。有些编程语言提供了更复杂的类型系统和模式匹配功能,可能可以减少一些样板代码。 -
可能存在更复杂的映射逻辑,允许输入映射到一个包含一或多个输出值的列表。这会根据您的编程语言和类型系统的灵活性而异。有些编程语言支持更高级的类型系统,可以更容易地表示这种复杂的映射逻辑。在这种情况下,您可以自定义类型或使用更复杂的模式匹配来实现所需的逻辑。
请注意,具体的实现方式会根据您所使用的编程语言和库而异。如果您有特定的编程语言和库的需求,可以提供更详细的信息,以便获得更具体的建议。
英文:
These are simple representations of sample Input and Output types:
Input = I1 Int | I2 String
Output = OA String | OB Bool | OC
Parameters here are just for the sake of greater realism.
I would like to get a function that maps Input
to Output
:
inputToOutput = \case
I1 val -> OA (show val)
I2 str -> (OB (str == "x"))
But this function should be typed checked against allows maps (I1 -> OB
,I2 -> OB
), so I could NOT do:
inputToOutput = \case
I1 val -> OB True -- allows only OA
I2 str -> OA str -- allows only OB
I have a solution variant with GADTs and Families, here I have to introduce additional tags for each of Input
and Output
values:
-- 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"))
-
My first question: is this the only way to achieve what I want (Using GADTs/Families)? what I don't like there, that I need to introduce additional boilerplate tags for
Input/Output
values, is it possible to make it less boilerplaty way? -
My second question: is a more advanced logic of mapping possible? Say I want the input to be mapped to a list of outputs that is required to contain one/serveral of the values:
inputToOutput = \case
I1 val -> [ OA (show val), OC] -- also allows other Output values like OC, but not requires
I2 str -> [(OB (str == "x"))]
答案1
得分: 3
以下是翻译好的内容:
要实现你的目标,最简单的方法似乎是这样的,这也是我在实际应用中可能会使用的方法:只需实现两个函数
i1case :: Int -> String
i2case :: String -> Bool
然后将其定义为
inputToOutput = \case
I1 val -> OA $ i1case val
I2 str -> OB $ i2case str
如果使用包含元素的类型作为健全性检查太弱,你可以随时添加新类型包装器,这也许是个好主意。
与你的标签相比,这仍然有一些限制。这种方法确实有意义。它需要一些样板代码,是的。原则上,你实际上不需要为标签定义新类型,你也可以只是使用
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。如果你可以接受仅“合理高概率”捕捉到任何违规行为,那么 QuickCheck 可以更容易地完成任务。
英文:
The simplest way to achieve your goal seems to be this, which is also what I would probably use in practice: just implement two functions
i1case :: Int -> String
i2case :: String -> Bool
and then make it
inputToOutput = \case
I1 val -> OA $ i1case val
I2 str -> OB $ i2case str
If using the type of the contained elements as a sanity check is too weak, you can always add newtype wrappers, which would perhaps be a good idea anyway.
This still has some limitations compared to your tags. That approach could certainly make sense too. It requires some boilerplate, yes. In principle you don't actually need to define fresh types for the tags, you could also just use
data Input (i :: Symbol) where
I1 :: Int -> Input "I1"
I2 :: String -> Input "I2"
etc., but I wouldn't actually recommend this.
As for your second question,
> is a more advanced logic of mapping possible? Say I want the input to be mapped to a list of outputs that is required to contain one/serveral of the values
– well, instead of trying to require a list to “contain one” or more, you could simply require that one right there and then, plus additional a list of outputs whose type you don't care about. For the latter you can use a simple existential wrapper,
data SomeOutput where
SomeOutput :: Output o -> SomeOutput
and then
inputToOutput :: Input a -> (Output (I2O a), [SomeOutput])
inputToOutput = \case
I1 val -> (OA (show val), [SomeOutput OC])
I2 str -> (OB (str == "x"), [])
More complicated requirements, like “at most three of this constructor”, are possible too, but this would get rather painful to express. Starting from some
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 = ...
you might get it to work, but you'd need to use of a lot of singletons
machinery to make it feasible. I'd probably not bother, and rather check the invariants with QuickCheck instead. Types are great, but their true strength is when they can actually help finding the right solutions and express intent. When you just want to forbid some kinds of code, types aren't a very effective tool, at least not in Haskell. In case you really need water-tight proofs, it's not the right language anyway, use Agda / Coq / Idris / Lean. If you're OTOH ok with merely reasonably high probability of catching any violations, QuickCheck gets the job done so much easier.
答案2
得分: 3
I think for this particular case, is fine with only Output tags which simplifies drastically. The approach is "tag each input and output with the output tag of desire"
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")
here you have the snippet for this code. Probably you can extend the functionality with some not-so-complex type family, but I am not that familiar with this level of Haskell. I guess you can do something like
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 something 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")
英文:
I think for this particular case, is fine with only Output tags which simplifies drastically. The approach is "tag each input and output with the output tag of desire"
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")
here you have the snipet for this code. Probably you can extend the functionality with some not-so-complex type family, but I am not that familiar with this level of haskell. I guess you can do something like
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")
通过集体智慧和协作来改善编程学习和解决问题的方式。致力于成为全球开发者共同参与的知识库,让每个人都能够通过互相帮助和分享经验来进步。
评论