Recreating Lisp's `apply` in Haskell using GADTs

As an exercise I'm trying to recreate Lisp's apply in Haskell. I do not intend to use this for any practical purpose, I just think it's a nice opportunity to get more familiar with Haskell's type system and type systems in general. (So I am also not looking for other people's implementations.)

My idea is the following: I can use GADTs to "tag" a list with the type of the function it can be applied to. So, I redefine Nil and Cons in a similar way that we would encode list length in the type using a Nat definition, but instead of using Peano numbers the length is in a way encoded in the tagging function type (i.e. length corresponds to the number of arguments to the function).

Here is the code I have so far:

{-# LANGUAGE GADTs #-}

-- n represents structure of the function I apply to
-- o represents output type of the function
-- a represents argument type of the function (all arguments same type)
data FList n o a where
  -- with Nil the function is the output
  Nil :: FList o o a
  -- with Cons the corresponding function takes one more argument
  Cons :: a -> FList f o a -> FList (a -> f) o a

args0 = Nil :: FList Int Int Int -- will not apply an argument
args1 = Cons 1 args0 -- :: FList (Int -> Int) Int Int
args2 = Cons 2 args1 -- :: FList (Int -> Int -> Int) Int Int
args3 = Cons 3 args2 -- :: FList (Int -> Int -> Int -> Int) Int Int

listApply :: (n -> o) -> FList (n -> o) o a -> o
-- I match on (Cons p Nil) because I always want fun to be a function (n -> o)
listApply fun (Cons p Nil) = fun p
listApply fun (Cons p l) = listApply (fun p) l

main = print $ listApply (+) args2

In the last line, my idea would be that (+) will be of type Int -> Int -> Int, where Int -> Int corresponds to the n in (n -> o) and o corresponds to the last Int (the output) [1]. As far as I can tell, this type seems to work out with the type of my argsN definitions.

However, I get two errors, of which I will state the component that seems relevant to me:

test.hs:19:43:
    Could not deduce (f ~ (n0 -> f))
    from the context ((n -> o) ~ (a -> f))
      bound by a pattern with constructor
                 Cons :: forall o a f. a -> FList f o a -> FList (a -> f) o a,
               in an equation for ‘listApply’

and

test.hs:21:34:
    Couldn't match type ‘Int’ with ‘Int -> Int’
    Expected type: FList (Int -> Int -> Int) (Int -> Int) Int
      Actual type: FList (Int -> Int -> Int) Int Int
    In the second argument of ‘listApply’, namely ‘args2’

I'm not sure how to interpret the first error. The second error is confusing me since it does not match with my interpretation stated marked with [1] earlier.

Any insights into what is going wrong?

P.S: I'm more than willing to learn about new extensions if that would make this work.

Solution

You got it almost right. Recursion should follow the structure of GADT:

{-# LANGUAGE GADTs #-}
-- n represents structure of the function I apply to
-- o represents output type of the function
-- a represents argument type of the function (all arguments same type)
data FList n o a where
  -- with Nil the function is the output
  Nil :: FList o o a
  -- with Cons the corresponding function takes one more argument
  Cons :: a -> FList f o a -> FList (a -> f) o a

args0 = Nil :: FList Int Int Int -- will not apply an argument
args1 = Cons 1 args0 -- :: FList (Int -> Int) Int Int
args2 = Cons 2 args1 -- :: FList (Int -> Int -> Int) Int Int
args3 = Cons 3 args2 -- :: FList (Int -> Int -> Int -> Int) Int Int

-- n, not (n -> o)
listApply :: n -> FList n o a -> o
listApply fun Nil = fun
listApply fun (Cons p l) = listApply (fun p) l

main = print $ listApply (+) args2

three :: Int
three = listApply (+) (Cons 2 (Cons 1  Nil))

oof :: String
oof = listApply reverse (Cons "foo" Nil)

true :: Bool
true = listApply True Nil -- True

-- The return type can be different than the arguments:

showplus :: Int -> Int -> String
showplus x y = show (x + y)

zero :: String
zero = listApply showplus (Cons 2 (Cons 1 Nil))

Must say, that this looks quite elegant!

Even OP doesn't ask for other's people implementation. You can approach problem a bit differently, resulting in a different looking but neat API:

{-# LANGUAGE KindSignatures #-}
{-# LANGuAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE AllowAmbiguousTypes #-}

import Data.Proxy

data N = O | S N

p0 :: Proxy O
p1 :: Proxy (S O)
p2 :: Proxy (S (S O))
p0 = Proxy
p1 = Proxy
p2 = Proxy

type family ArityNFun (n :: N) (a :: *) (b :: *) where
  ArityNFun O a b = b
  ArityNFun (S n) a b = a -> ArityNFun n a b

listApply :: Proxy n -> ArityNFun n a b -> ArityNFun n a b
listApply _ = id

three :: Int
three = listApply p2 (+) 2 1

oof :: String
oof = listApply p1 reverse "foo"

true :: Bool
true = listApply p0 True

showplus :: Int -> Int -> String
showplus x y = show (x + y)

zero :: String
zero = listApply p2 showplus 0 0

Here we could use Nat from GHC.TypeLits, but then we'd need UndecidableInstances. The added sugar is not worth the trouble in this example.

If you want to make polymorphic version, that's also possible, but then index is not (n :: Nat) (a :: *) but (as :: [*]). Also making plusN could be a nice exercise, for both encodings.