Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Is it possible to reorganize nested tuples?

Tags:

haskell

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.

like image 405
DantheMan Avatar asked Dec 08 '22 16:12

DantheMan


1 Answers

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")]
like image 60
Stefan Holdermans Avatar answered Dec 21 '22 10:12

Stefan Holdermans