What I want to do is something like this:
Take an arbitrary polymorphic tuple:
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, ()))))
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))
to
(Int, (Char, (Maybe Int, (String, (Int, ()))))
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, ()))))
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 #-}
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
of type
U (Int, (Char, (Maybe Int, (String, (Int, ()))))
As a convenience, we introduce
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
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.
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))
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)
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)
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)]
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']
As an example, we have that
conv (Int :*: Char) (Char :*: Int) (2, 'x')
yields
[('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
then
from (((1, ""), Nothing), (' ', 6))
yields
[ (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
Then, for example
conv' ("foo", 'x') :: [((Char, ()), String)]
yields
[(('x', ()), "foo")]
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With