Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

What is the easiest way to turn a list with known length into nested pairs in Haskell?

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.

like image 582
Rehno Lindeque Avatar asked Nov 28 '22 23:11

Rehno Lindeque


2 Answers

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.

like image 180
Daniel Wagner Avatar answered Dec 05 '22 04:12

Daniel Wagner


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)
like image 24
András Kovács Avatar answered Dec 05 '22 03:12

András Kovács