How should one convert a list with a known length into nested pairs? In other words, what is the most convenient way to fill the type holes below?
_ [1,2] :: (Int,Int)
_ [1,2,3] :: ((Int,Int),Int)
_ [1,2,3,4] :: (((Int,Int),Int),Int)
_ [1,2,3,4,5] :: ((((Int,Int),Int),Int),Int)
EDIT: note that the type holes need not be the same function, I'm looking for a convenient pattern (if a convenient pattern exists) to fill the holes.
Perhaps like this:
step f xs = (f (init xs), last xs)
len1 = head
len2 = step len1
len3 = step len2
len4 = step len3
In ghci:
*Main> len4 [1..4]
(((1,2),3),4)
One may of course also directly implement one of these functions with pattern matching:
len4' [a,b,c,d] = (((a,b),c),d)
This will also not traverse the list as many times as there are elements, which is nice.
Chiming in with a dependently typed version. First, let's get done with the boilerplate:
{-# LANGUAGE
TemplateHaskell, DataKinds, ScopedTypeVariables,
FlexibleInstances, PolyKinds, TypeOperators,
TypeFamilies, GADTs, UndecidableInstances #-}
import Data.Singletons.TH
import qualified GHC.TypeLits as Lit
$(singletons [d| data Nat = Z | S Nat deriving (Eq, Show) |])
The use of TH here is purely for boilerplate reduction and we won't use TH in our actual code. In fact, the above could be (and should be) factored out in a package somewhere (at the time of writing this answer there isn't such a package with up-to-date singletons dependency).
tuplify becomes a function whose return type depends on a Nat parameter.
type family NTup n a where
NTup (S (S Z)) a = (a, a)
NTup (S (S (S n))) a = (NTup (S (S n)) a, a)
tuplify :: Sing n -> [a] -> NTup n a
tuplify n as = go n (reverse as) where
go :: Sing n -> [a] -> NTup n a
go (SS (SS SZ)) [a, b] = (b, a)
go (SS (SS (SS n))) (a:as) = (go (SS (SS n)) as, a)
go _ _ = error "tuplify: length mismatch"
Trying it out:
tuplify (SS (SS (SS SZ))) [1, 2, 3] -- ((1, 2), 3)
Writing out the naturals is quite arduous now, so let's introduce some syntactic sugar:
type family N n where
N 0 = Z
N n = S (N (n Lit.- 1))
type SN n = Sing (N n)
Now:
tuplify (sing:: SN 10) [1..10] -- (((((((((1,2),3),4),5),6),7),8),9),10)
As a side note, if we convert the empty list to () (and thereby also allow one-element nested tuples) our definitions become much more natural:
type family NTup n a where
NTup Z a = ()
NTup (S n) a = (NTup n a, a)
tuplify :: Sing n -> [a] -> NTup n a
tuplify n = go n . reverse where
go :: Sing n -> [a] -> NTup n a
go SZ [] = ()
go (SS n) (a:as) = (go n as, a)
go _ _ = error "tuplify: length mismatch"
tuplify (sing:: SN 5) [1..5] -- ((((((),1),2),3),4),5)
This would be a nice exercise in Agda with dependent types. In Haskell you can achieve something close with (also inspired from Daniel Wagner's solution)
class C a b where
listToTuple :: [a] -> b
instance C a a where
listToTuple [x] = x
instance C a b => C a (b,a) where
listToTuple xs = (listToTuple (init xs), last xs)
Some tests:
> listToTuple [1..3::Int] :: ((Int,Int),Int)
((1,2),3)
> listToTuple [0..3::Int] :: (((Int,Int),Int),Int)
(((0,1),2),3)
Note that the return type annotation is mandatory, otherwise Haskell can not deduce how many elements the return tuple must have. If there is a mismatch between the tuple and list length, a run-time error occurs. This is pretty much unavoidable since lists do not carry their length in their type, so the compiler can not check this earlier (unlike using a vector GADT).
In order to have such a generic and type-safe function, you'd need dependent types so that the number of nested tuples in the result could depend on the length of the input list.
However it's possible to get close to that with polymorphic recursion.
Let's define a data type as follows:
data TupleList' r a = Value r | Tuple (TupleList' (r, a) a)
deriving (Show, Read, Eq, Ord)
type TupleList = TupleList' ()
So a value of type TupleList a is isomorphic to (), ((), a), (((), a), a) etc, depending on how many Tuple constructors wrap the final Value.
Now we can convert a list into such a tuple as follows:
fromList :: [a] -> TupleList a
fromList = loop ()
where
loop :: r -> [a] -> TupleList' r a
loop r [] = Value r
loop r (x:xs) = Tuple (loop (r, x) xs)
Notice that loop uses polymorphic recursion (as any function that operates on TupleList' - its recursive call has signature (r, a) -> [a] -> TupleList' (r, a) a.
Example: mapM_ (print . fromList) (inits [1..4]) yields
Value ()
Tuple (Value ((),1))
Tuple (Tuple (Value (((),1),2)))
Tuple (Tuple (Tuple (Value ((((),1),2),3))))
Tuple (Tuple (Tuple (Tuple (Value (((((),1),2),3),4)))))
The simplest way is
z (x:xs) = x
s r (x:xs) = (x, r xs)
toTuples n xs = n xs
But toTuples returns pairs in the reverse order:
toTuples (s (s (s z))) [1..] == (1,(2,(3,4)))
We can use CPS to fix this:
z f xs = f ()
s r f (x:xs) = r (\p -> (f p, x)) xs
toTuples n (x:xs) = n (const x) xs
Then
toTuples (s (s (s z))) [1..] == (((1,2),3),4)
And we can define some syntactic sugar (I'm mostly stealing from András Kovács' answer):
{-# LANGUAGE TemplateHaskell, UndecidableInstances, DataKinds, GADTs, TypeFamilies, TypeOperators #-}
import Data.Singletons.TH
import GHC.TypeLits
$(singletons [d| data Nat = Z | S Nat deriving (Eq, Show) |])
z f xs = f ()
s r f (x:xs) = r (\p -> (f p, x)) xs
toTuples n (x:xs) = n (const x) xs
type family Result n r a where
Result Z r a = r
Result (S n) r a = Result n (r, a) a
run :: Sing n -> (() -> r) -> [a] -> Result n r a
run SZ = z
run (SS sn) = s (run sn)
toTuplesN :: Sing n -> [a] -> Result n a a
toTuplesN sn (x:xs) = run sn (const x) xs
type family N n where
N 0 = Z
N n = S (N (n - 1))
type SN n = Sing (N (n - 1))
main = print $ toTuplesN (sing :: SN 6) [1..] -- (((((1,2),3),4),5),6)
Note that the code works for infinite lists too, since there is no reversing.
