How to convert type-level list into chain of pairs

Question

The singletons library seems too difficult to deal with it without strong background. Is there any way to convert level typed list like '[1, 2, 3] into chain of pairs like '(1, '(2, '(3, '())))?

I've tried to write few lines but they produce expressionless for me errors.

{-# LANGUAGE TypeFamilies, TypeInType #-}

module ExpandList where

import Data.Singletons.Prelude.List
import Data.Singletons.Prelude.Tuple

type family IntoChainOfPairs (xs :: [k]) :: (k, b) where
  IntoChainOfPairs (x ': '[]) = '(x, '())
  IntoChainOfPairs (x ': xs) = '(x, IntoChainOfPairs xs)

sIntoChainOfPairs :: forall a (t :: [a]). Sing t -> Sing (IntoChainOfPairs t)
sIntoChainOfPairs = \case
  SCons a SNil -> STuple2 a STuple0
  SCons a b -> STuple2 a (sIntoChainOfPairs b)

So I stacked in fundamental misunderstanding. Compiler doesn't understand me, I don't understand it. I'm sure my code is wrong at the root.

Answer 1

The type of IntoChainOfPairs's result should change with the input. Therefore, there are actually two functions, one type ToPairsType (xs :: [a]) :: Type—computing the output type from the input—and one type ToPairs (xs :: [a]) :: ToPairsType xs—actually computing the output.

type family ToPairsType (xs :: [a]) :: Type where
  ToPairsType '[] = ()
  ToPairsType ((_ :: a) : xs) = (a, ToPairsType xs)
type family ToPairs (xs :: [a]) :: ToPairsType xs where
  ToPairs '[] = '()
  ToPairs (x : xs) = '(x, ToPairs xs)

You defined a single partial function, where b was an argument to IntoChainOfPairs. You really wrote

type family IntoChainOfPairs (k :: Type) (b :: Type) (xs :: [k]) :: (k, b) where
  IntoChainOfPairs k () (x : '[]) = '(x, '())
  IntoChainOfPairs k (k, b') (x : xs) = '(x, IntoChainOfPairs k b' xs)

Where you had partial pattern matching on b, with nonlinear matching on k. Additionally, the unnatural (partial!) list-processing does not help. You can sorta-maybe-painfully get value-level case on Types, using the Typeable infrastructure, for writing sIntoChainOfPairs, but I would not advise it. Really, IntoChainOfPairs is just broken.

sToPairs is written as a direct "reflection" of ToPairs:

sToPairs :: forall (a :: Type) (xs :: [a]). Sing xs -> Sing (ToPairs xs)
sToPairs SNil = STuple0
sToPairs (SCons x xs) = STuple2 x (sToPairs xs)