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)
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