peano.hs

{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE DataKinds          #-}
{-# LANGUAGE TypeOperators          #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances     #-}

import GHC.TypeLits
import Data.Proxy

type family Last (a :: (Nat -> *)) :: Nat
newtype VJ (t :: Nat -> *) (v :: Nat) = VJ Int
data D (v :: Nat)

class Op (t :: Nat -> *) (v :: Nat) where
    f :: VJ t v -> VJ t (Last t)

instance Op D 0 where
    f (VJ i) = f (VJ i :: VJ D (0+1))

instance Op D 1 where
    f (VJ i) = VJ i

main = do
  putStrLn "hello"

data Zero
data Succ a
type family Last' (a :: (* -> *)) :: *
data D' v
type instance Last' D' = Succ Zero
newtype VJ' (t :: * -> *) v = VJ' Int

class Op' (t :: * -> *) v where
    f' :: VJ' t v -> VJ' t (Last' t)

instance Op' D' Zero where
    f' (VJ' i) = f' (VJ' i :: VJ' D' (Succ Zero))

instance Op' D' (Succ Zero) where
    f' (VJ' i) = VJ' i