ZipWith.hs

-- http://www.cis.upenn.edu/~eir/papers/2014/axioms/axioms-extended.pdf
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE ScopedTypeVariables   #-}

module ZipWith (zipWith) where

data Nat
  = Zero
  | Succ Nat

type family Listify (n :: Nat) arrows where
  Listify Zero     a        = [a]
  Listify (Succ n) (a -> b) = [a] -> Listify n b

data NumArgs :: Nat -> * -> * where
  NAZero ::                NumArgs Zero     a
  NASucc :: NumArgs n b -> NumArgs (Succ n) (a -> b)

listApply :: NumArgs n a -> [a] -> Listify n a
listApply NAZero      fs = fs
listApply (NASucc na) fs =
  \args -> listApply na (apply fs args)
  where
  apply :: [a -> b] -> [a] -> [b]
  apply (f : fs) (x : xs) = f x : apply fs xs
  apply _        _        = []

type family CountArgs (f :: *) :: Nat where
  CountArgs (a -> b) = Succ (CountArgs b)
  CountArgs result   = Zero

class CNumArgs (numArgs :: Nat) (arrows :: *) where
  getNA :: NumArgs numArgs arrows

instance CNumArgs Zero a  where
  getNA = NAZero

instance CNumArgs n b =>
         CNumArgs (Succ n) (a -> b) where
  getNA = NASucc getNA

zipWith :: forall f. CNumArgs (CountArgs f) f
        => f -> Listify (CountArgs f) f
zipWith fun = listApply (getNA :: NumArgs (CountArgs f) f) (repeat fun)