gistfile1.hs

{-# Language GADTs, KindSignatures, DataKinds, TypeOperators, TypeFamilies #-}
data Nat = Zero | Succ Nat
data SNat (n :: Nat) where
    SZero :: SNat 'Zero
    SSucc :: SNat m -> SNat ('Succ m)

type family NIntArrow (a :: Nat)
type instance NIntArrow 'Zero = Int
type instance NIntArrow ('Succ n) = Int -> NIntArrow n

addN :: SNat nat -> NIntArrow nat
addN n = addN' n 0
    where
      addN' :: SNat nat -> Int -> NIntArrow nat
      addN' SZero acc = acc
      addN' (SSucc n') acc = \x -> addN' n' (acc+x)

>>> addN (SSucc (SSucc (SSucc SZero))) 1 2 4
7
>>> addN SZero
0