an example for type level addition

peano.hs

-----------------------------------------------------------------------------
--
-- Module      :  Peano
-- Copyright   :  2017 Author name here
-- License     :  BSD3
--
-- Maintainer  :  example@example.com
-- Stability   :
-- Portability :
--
-- | used https://byorgey.wordpress.com/2010/06/29/typed-type-level-programming-in-haskell-part-i-functional-dependencies/
--
-----------------------------------------------------------------------------
{-# OPTIONS_GHC -F -pgmF htfpp #-}

{-# LANGUAGE  MultiParamTypeClasses    #-}
{-# LANGUAGE  TypeFamilies    #-}
{-# LANGUAGE FunctionalDependencies    #-}
{-# LANGUAGE GADTs    #-}
{-# LANGUAGE FlexibleInstances   #-}
{-# LANGUAGE OverloadedStrings   #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# OPTIONS_GHC -fno-warn-missing-methods #-}
{-# OPTIONS_GHC -fno-warn-missing-signatures #-}
{-# OPTIONS_GHC -w #-}

module Peano (module Peano

    ) where

import Test.Framework
import           Uniform.Strings
--import Data.HList.HListTF


data Z
data S n

type family Plus m n :: *
type instance Plus Z n = n
type instance Plus (S m) n = S (Plus m n)

z0 = undefined :: Z
o1 = undefined :: S Z
t2 = undefined :: S (S Z)

t2'=  undefined :: Plus (S Z) (S (S Z))  -- 1 plus 2



example1 :: IO ()
example1 = do
        putIOwords ["example1"]
--        let s = show t2'
        -- gives error : No instance for (Show (S (S (S Z))))
        --        arising from a use of ‘show’
        return ()

-- list with length as a type
data LOL :: * -> * -> * where
    MkSingleton :: LOL Z a
    LolAddEl    :: a -> LOL n a -> LOL (S n) a

append2 :: LOL m a -> LOL n a -> LOL (Plus m n) a
append2 MkSingleton     v = v
--append2 (LolAddEl x xs) v = LolAddEl x (append xs v)

--l0 = undefined :: MkSingleton  Int