Recreating Lisp's `apply` in Haskell using GADTs

Question

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…

Accepted Answer

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.

Recreating Lisp's `apply` in Haskell using GADTs

Solution

Problem

Related problems