Generate function of given arity in Haskell using type numbers

haskell, type-level-computation, types, variadic-functions

Solution

OK. Yes. Definitely, by threading a numeric type around the recursive instances.

First, some boilerplate:

{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE MultiParamTypeClasses  #-}
{-# LANGUAGE EmptyDataDecls         #-}
{-# LANGUAGE FlexibleInstances      #-}
{-# LANGUAGE FlexibleContexts       #-}
{-# LANGUAGE ScopedTypeVariables    #-}

Your nats:

data Zero
data Succ n

A recursive builder for the variadic functions, now with an n argument:

class BuildList n a r | r -> a where
    build' :: n -> [a] -> a -> r

A base case: stop when we get to `Zero`:

instance BuildList Zero a [a] where
    build' _ l x = reverse $ x:l

Otherwise, decrement by one and recurse:

instance BuildList n a r => BuildList (Succ n) a (a->r) where
    build' (_ :: Succ n) l x y = build' (undefined :: n) (x:l) y

Now, we only want to loop 3 times, so write that down:

build :: BuildList (Succ (Succ Zero)) a r => a -> r
build x = build' (undefined :: Succ (Succ Zero)) [] x

Done.

Testing:

> build "one" "two" "three" :: [[Char]]
["one","two","three"]

Any less or more are errors:

*Main> build "one" "two" "three" "four" :: [[Char]]

<interactive>:1:1:
    No instance for (BuildList Zero [Char] ([Char] -> [[Char]]))

*Main> build "one" "two" :: [[Char]]

<interactive>:1:1:
    No instance for (BuildList (Succ Zero) [Char] [[Char]])

Problem

Assume I have encoded the natural numbers in Haskell types, and that I have a way of adding and subtracting from them: ``` data Zero data Succ n -- ... ``` I have seen various bits of code which create the appearance of variadic functions, such as this, which allows the following: ``` buildList "polyvariadic" "function" "wut?" :: [String] -- ["polyvariadic","function","wut?"] ``` What I am wondering is whether I can build off of that to make a function which will only accept the number of arguments that corresponds to an instance of a type number. What I'm trying to do would look something like: ``` one = Succ Zero two = Succ one three = Succ two threeStrings :: String -> String -> String -> [String] threeStrings = buildList three threeStrings "asdf" "asdf" "asdf" -- => ["asdf","asdf","asdf"] threeStrings "asdf" -- type checker is all HOLY CHRIST TYPE ERROR threeStrings "asdf" "asdf" "asdf" "asdf" -- type checker is all SWEET JESUS WHAT YOU ARE DOING ``` I'm aware that this is pretty silly and that it's probably a waste of my time, but it seemed like something that would be fun for the weekend.

Original source