是否可以重组嵌套元组? [英] Is it possible to reorganize nested tuples?
问题描述
我想做的是这样的:
采用任意多态元组:
x = (((1, ""), Nothing), ('', 6))
并用这种类型的东西进行重组(不一定要按相同的顺序，但要使用相同的结构.
And reorganize with something like this type (not necessarily in the same order but the same structure.:
(Int, (Char, (Maybe Int, (String, (Int, ()))))
我真的不知道这种模式的名称，所以我无法尽我所能使用Google.
I really don't know the name for this pattern so I am unable to use google to the best of my ability.
推荐答案
如果您只需要处理这种特殊情况，即转换为
If you only have to deal with this specific case, i.e., converting from
(((Int, String), Maybe Int), (Char, Int))
到
(Int, (Char, (Maybe Int, (String, (Int, ()))))
然后，根据要保留Int -component的顺序还是交换它们，只需使用以下两个函数之一即可:
then, depending on whether you want to preserve the order of the Int-components or swap them, you can simply use one of these two functions:
from1 (((m, s), mb), (c, n)) = (m, (c, mb, (s, (n, ()))))
from2 (((m, s), mb), (c, n)) = (n, (c, mb, (s, (m, ()))))
但是我们当然可以更具野心，并寻求更通用的解决方案；参见例如 Jeuring和Atanassow(MPC 2004).为此，让我们启用一些语言扩展
But we can of course be just a bit more ambitious and aim for a more generic solution; see, for example, Jeuring and Atanassow (MPC 2004). To this end, let us enable some language extensions
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
并介绍用于表示元组类型的代码的GADT
and introduce a GADT for codes that we can use to represent tuple types
infixr 5 :*:
data U a where
Unit :: U ()
Int :: U Int
Char :: U Char
List :: U a -> U [a]
Maybe :: U a -> U (Maybe a)
(:*:) :: U a -> U b -> U (a, b)
例如，您示例中的目标类型现在可以由表达式编码
For example, the target type from your example can now be encoded by the expression
Int :*: Char :*: Maybe Int :*: string :*: Int :*: Unit
类型
U (Int, (Char, (Maybe Int, (String, (Int, ()))))
为方便起见，我们介绍
string :: U String
string = List Char
我们进一步介绍了一种显式类型化的元组值
We furthermore introduce a type of explicitly typed tuple values
data Typed where
Typed :: U a -> a -> Typed
和类型级别相等的概念:
and a notion of type-level equality:
infix 4 :==:
data a :==: b where
Refl :: a :==: a
这样，我们可以在元组类型的编码上定义异构检查:
With that, we can define a heterogeneous equality check on tuple-type encodings:
eq :: U a -> U b -> Maybe (a :==: b)
eq Unit Unit = Just Refl
eq Int Int = Just Refl
eq Char Char = Just Refl
eq (List u1) (List u2) = case eq u1 u2 of
Just Refl -> Just Refl
_ -> Nothing
eq (Maybe u1) (Maybe u2) = case eq u1 u2 of
Just Refl -> Just Refl
_ -> Nothing
eq (u11 :*: u12) (u21 :*: u22) = case (eq u11 u21, eq u12 u22) of
(Just Refl, Just Refl) -> Just Refl
_ -> Nothing
eq _ _ = Nothing
如果u1和u2编码相同的元组类型，则eq u1 u2返回Just Refl，否则返回Nothing.在Just情况下，构造函数Refl充当类型检查器的证明，即元组类型确实相同.
That is eq u1 u2 returns Just Refl if u1 and u2 encode the same tuple type, and Nothing otherwise. In the Just-case the constructor Refl acts as proof for the type checker that the tuple types are indeed the same.
现在，我们希望能够将元组类型转换为扁平化"(即右嵌套)表示形式.为此，我们介绍了一个类型族Flatten:
Now we want to be able to convert tuple types to a "flattened", i.e., right-nested, representation. For this, we introduce a type family Flatten:
type family Flatten a
type instance Flatten () = ()
type instance Flatten Int = Flatten (Int, ())
type instance Flatten Char = Flatten (Char, ())
type instance Flatten [a] = Flatten ([a], ())
type instance Flatten (Maybe a) = Flatten (Maybe a, ())
type instance Flatten ((), a) = Flatten a
type instance Flatten (Int, a) = (Int, Flatten a)
type instance Flatten (Char, a) = (Char, Flatten a)
type instance Flatten ([a], b) = ([a], Flatten b)
type instance Flatten (Maybe a, b) = (Maybe a, Flatten b)
type instance Flatten ((a, b), c) = Flatten (a, (b, c))
和两个函数flattenV和flattenU分别用于展平元组值及其类型的编码:
and two functions flattenV and flattenU for, respectively, flattening tuple values and the encodings of their types:
flattenV :: U a -> a -> Flatten a
flattenV Unit _ = ()
flattenV Int n = flattenV (Int :*: Unit) (n, ())
flattenV Char c = flattenV (Char :*: Unit) (c, ())
flattenV (List u) xs = flattenV (List u :*: Unit) (xs, ())
flattenV (Maybe u) mb = flattenV (Maybe u :*: Unit) (mb, ())
flattenV (Unit :*: u) (_, x) = flattenV u x
flattenV (Int :*: u) (n, x) = (n, flattenV u x)
flattenV (Char :*: u) (c, x) = (c, flattenV u x)
flattenV (List _ :*: u) (xs, x) = (xs, flattenV u x)
flattenV (Maybe _ :*: u) (mb, x) = (mb, flattenV u x)
flattenV ((u1 :*: u2) :*: u3) ((x1, x2), x3)
= flattenV (u1 :*: u2 :*: u3) (x1, (x2, x3))
flattenU :: U a -> U (Flatten a)
flattenU Unit = Unit
flattenU Int = Int :*: Unit
flattenU Char = Char :*: Unit
flattenU (List u) = List u :*: Unit
flattenU (Maybe u) = Maybe u :*: Unit
flattenU (Unit :*: u) = flattenU u
flattenU (Int :*: u) = Int :*: flattenU u
flattenU (Char :*: u) = Char :*: flattenU u
flattenU (List u1 :*: u2) = List u1 :*: flattenU u2
flattenU (Maybe u1 :*: u2) = Maybe u1 :*: flattenU u2
flattenU ((u1 :*: u2) :*: u3) = flattenU (u1 :*: u2 :*: u3)
然后将两者合并为一个函数flatten:
The two are then combined into a single function flatten:
flatten :: U a -> a -> Typed
flatten u x = Typed (flattenU u) (flattenV u x)
我们还需要一种方法来从展平表示中恢复元组组件的原始嵌套:
We also need a way to recover the original nesting of tuple-components from a flattened representation:
reify :: U a -> Flatten a -> a
reify Unit _ = ()
reify Int (n, _) = n
reify Char (c, _) = c
reify (List u) (xs, _) = xs
reify (Maybe u) (mb, _) = mb
reify (Unit :*: u) y = ((), reify u y)
reify (Int :*: u) (n, y) = (n, reify u y)
reify (Char :*: u) (c, y) = (c, reify u y)
reify (List _ :*: u) (xs, y) = (xs, reify u y)
reify (Maybe _ :*: u) (mb, y) = (mb, reify u y)
reify ((u1 :*: u2) :*: u3) y = let (x1, (x2, x3)) = reify (u1 :*: u2 :*: u3) y
in ((x1, x2), x3)
现在，给定元组组件的类型代码u和扁平化的元组以及其类型的编码，我们定义函数select，该函数返回所有可能的方式从元组中选择类型为匹配u和其余组件的展平表示形式:
Now, given a type code u for a tuple component and a flattened tuple together with an encoding of its type, we define function select that returns all possible ways to select from the tuple a component with a type that matches u and a flattened representation of the remaining components:
select :: U b -> Typed -> [(b, Typed)]
select _ (Typed Unit _) = []
select u2 (Typed (u11 :*: u12) (x1, x2)) =
case u11 `eq` u2 of
Just Refl -> (x1, Typed u12 x2) : zs
_ -> zs
where
zs = [(y, Typed (u11 :*: u') (x1, x')) |
(y, Typed u' x') <- select u2 (Typed u12 x2)]
最后，我们可以定义一个函数conv，该函数接受两个元组类型的代码和一个与第一个代码相匹配的类型的元组，然后将所有可能的转换返回到与第二个代码相匹配的类型的元组中:
Finally, we can then define a function conv that takes two tuple-type codes and a tuple of a type that matches the first code, and returns all possible conversions into a tuple of a type that matches the second code:
conv :: U a -> U b -> a -> [b]
conv u1 u2 x = [reify u2 y | y <- go (flattenU u2) (flatten u1 x)]
where
go :: U b -> Typed -> [b]
go Unit (Typed Unit _ ) = [()]
go (u1 :*: u2) t =
[(y1, y2) | (y1, t') <- select u1 t, y2 <- go u2 t']
作为一个例子，我们有
conv (Int :*: Char) (Char :*: Int) (2, 'x')
收益
[('x', 2)]
如果您定义的话，请回到您的原始示例
Returning to your original example, if we define
from = conv u1 u2
where
u1 = ((Int :*: string) :*: Maybe Int) :*: Char :*: Int
u2 = Int :*: Char :*: Maybe Int :*: string :*: Int :*: Unit
然后
from (((1, ""), Nothing), (' ', 6))
收益
[ (1, (' ', (Nothing, ("", (6, ())))))
, (6, (' ', (Nothing, ("", (1, ())))))
]
通过引入可表示元组类型的类型类，我们可以使事情变得更好:
We can make things even a bit nicer, by introducing a type class for representable tuple types:
class Rep a where
rep :: U a
instance Rep () where rep = Unit
instance Rep Int where rep = Int
instance Rep Char where rep = Char
instance Rep a => Rep [a] where rep = List rep
instance Rep a => Rep (Maybe a) where rep = Maybe rep
instance (Rep a, Rep b) => Rep (a, b) where rep = rep :*: rep
这样，我们可以定义一个不需要元组的类型代码的转换函数:
That way, we can define a conversion function that does not need the type codes for the tuples:
conv' :: (Rep a, Rep b) => a -> [b]
conv' = conv rep rep
然后，例如
conv' ("foo", 'x') :: [((Char, ()), String)]
收益
[(('x', ()), "foo")]
这篇关于是否可以重组嵌套元组?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
