How to build a typed variadic function from a container?

Question

Consider the lovely little HoleyMonoid library, which lets you build typed variadic printf-like functions as follows:

{-# LANGUAGE NoMonomorphismRestriction #-}

import Control.Category
import Data.HoleyMonoid
import Prelude hiding ((.), id)

foo =
    now "hello "
  . later id
  . now ", you are "
  . later show
  . now " years old"

bar = run foo

-- > bar "alice" 42
-- "hello alice, you are 42 years old"

-- > bar 42 "alice"
-- type error

Is there any way to examine a container (a list, an AST, etc.) and build such a function based on its contents?

As a toy example, you can picture something like the following:

import Data.Monoid

adder = go where
  go [] = now (Sum 0)
  go (x:xs)
    | x == 5    = now 100 . go xs
    | otherwise = later id . go xs

-- hypothetical usage
--
-- > :t run adder [1, 3, 5]
-- Num a => Sum a -> Sum a -> Sum a
--
-- > getSum $ run adder [1, 3, 5] 0 1
-- 101

adder fails the occurs check, but you can see what I'm shooting for. The problem seems to be that it's difficult to hold the state of the computation anywhere, as i.e. now 100 and later id are at different types.

Answer 1

I'll ignore the HoleyMonoid library.

We need natural numbers:

data Nat = Z | S Nat

A singleton to lift them to the type level:

data Natty :: Nat -> * where
    Zy :: Natty Z
    Sy :: Natty n -> Natty (S n)

The type of lists of existentials:

data Listy (b :: a -> *) :: [a] -> * where
    Nilly :: Listy b '[]
    Consy :: b x -> Listy b xs -> Listy b (x ': xs)

Then with

type Natties = Listy Natty

We can define

adder :: Natties ns -> Adder ns

where ns :: [Nat]. The Adder type family is defined like this:

type family Adder (ns :: [Nat]) :: * where
    Adder '[]       = Int
    Adder (n ': ns) = If (NatEq n (S (S (S (S (S Z)))))) Int (Int -> Adder ns)

I.e. fold a list of Nats, prepending (Int ->) for each number in the list, until 5 (in a Nat form) is encountered. It actually should be something like

if_then_else_ b x y = if b then x else y

type family Adder (ns :: [Nat]) :: * where
    Adder '[]       = Int
    Adder (n ': ns) = 'if_then_else_ (n '== 'fromInt 5) Int (Int -> Adder ns)

but GHC throws at me some creepy errors, that I do not want to understand.

The NatEq type family is defined in the obvious way:

type family NatEq n m :: Bool where
    NatEq  Z     Z    = True
    NatEq  Z    (S m) = False
    NatEq (S n)  Z    = False
    NatEq (S n) (S m) = NatEq n m

We need to compare Nattys at the value level. Two Nattys are equal, iff they indexed by the same number (that's why Natty is a singleton):

nattyEq :: Natty n -> Natty m -> Booly (NatEq n m)
nattyEq  Zy     Zy    = Truly
nattyEq  Zy    (Sy m) = Falsy
nattyEq (Sy n)  Zy    = Falsy
nattyEq (Sy n) (Sy m) = nattyEq n m

Where Booly is another singleton:

data Booly :: Bool -> * where
    Truly :: Booly True
    Falsy :: Booly False

Finally, the definition of adder:

adder = go 0 where
    go :: Int -> Natties ns -> Adder ns
    go i  Nilly       = 0
    go i (Consy n ns) = case nattyEq n (Sy (Sy (Sy (Sy (Sy Zy))))) of
        Truly -> i + 100
        Falsy -> \a -> go (i + a) ns

I.e. sum all arguments, until 5 (in a Natty form) is encountered, and add 100. If there is no 5 in the list, then return 0.

Tests:

list = Consy Zy $ Consy (Sy Zy) $ Consy (Sy (Sy (Sy (Sy (Sy Zy))))) $ Consy Zy $ Nilly

main = do
    print $ adder (Consy Zy $ Consy (Sy Zy) $ Nilly) 3 9 -- 0
    print $ adder list 6 8                               -- 114
    print $ adder (Consy (Sy (Sy Zy)) list) 1 2 3        -- 106

The code.