Dependant Types Apply

README.md

Based on the zipWith example in Eisenberg's "Dependent Types in Haskell: Theory and Practice".

Allows you to convert a function f :: a -> a -> ... -> a -> r to a function f' :: b -> b -> ... b -> r

Apply.hs

{-# LANGUAGE NoImplicitPrelude #-}

module Apply where

import Data.Kind
import Data.Function
import Data.Int
import Data.Bool
import Prelude ((>))

data Nat = Zero | Succ Nat

type family Aify (n :: Nat) a b ty where
  Aify 'Zero _ _ ty = ty
  Aify ('Succ na) a b (b -> c) = a -> Aify na a b c

data NumArgs :: Nat -> Type -> Type -> Type where
  NAZero :: forall a b. NumArgs 'Zero a b
  NASucc :: forall a b (n :: Nat). NumArgs n a b -> NumArgs ('Succ n) a (a -> b)

aApply :: NumArgs n a f -> (b -> a) -> f -> Aify n b a f
aApply NAZero      _    f = f
aApply (NASucc na) conv f = \x ->  aApply na conv (f . conv $ x)

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

class CNumArgs (numArgs :: Nat) (a :: Type) (f :: Type) where
  getNA :: NumArgs numArgs a f

instance CNumArgs 'Zero a a where
  getNA = NAZero

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

eval :: forall a c f. CNumArgs (CountArgs f) a f
     => (c -> a) -> f -> Aify (CountArgs f) c a f
eval = aApply (getNA :: NumArgs (CountArgs f) a f)

example_1 = eval ((>0) :: Int -> Bool) (\a b c -> a && b && c) 1 0 3