. -, :
{-
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) |])
TH , TH . , ( ) - ( singletons).
tuplify , Nat.
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"
:
tuplify (SS (SS (SS SZ))) [1, 2, 3] -- ((1, 2), 3)
naturals , - :
type family N n where
N 0 = Z
N n = S (N (n Lit.- 1))
type SN n = Sing (N n)
:
tuplify (sing:: SN 10) [1..10] -- (((((((((1,2),3),4),5),6),7),8),9),10)
, () ( ), :
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)