{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeFamilies #-}



test1 = do let x = head (tail ([1]))
           print x

{-
-- Won't type check!
test2 = do let x = headSafe (tailSafe (Cons 1 Nil))
           print x
-}

-- Okay
test3 = do let x = headSafe (Cons 1 Nil)
           print x

main = do -- test1  -- program will crash
          return ()

-- Representing length-indexed lists in Haskell.

-- Natural numbers.
data Zero = Zero
data Succ n = Succ n

-- Length-indexed lists.
data List a n where
    Nil :: List a Zero
    Cons :: a -> List a m -> List a (Succ m)

-- All convenience functions also apply to "our" form of lists.
-- Haskell's "printf" via overloading.
instance Show a => Show (List a n) where
   show Nil = "[]"
   show (Cons x Nil) = "[" ++ show x ++ "]"
   show (Cons x xs) = "[" ++ show x ++ "," ++ tail (show xs)

-- List examples.
listNonEmpty1 = Cons False Nil
listNonEmpty2 = Cons True (Cons False Nil)
listEmpty = Nil

-- Safe operations on list.
headSafe :: List a (Succ n) -> a
headSafe (Cons x _) = x

tailSafe :: List a (Succ n) -> List a n
tailSafe (Cons _ xs) = xs

-- Reversing a list won't change its length.
reverseProp :: List a n -> List a n
reverseProp Nil = Nil
reverseProp (Cons x xs) = snoc (reverseProp xs) x

-- Helper snoc takes a list [x1,...,xn] and an element x
-- and yields the list [x1,...,xn,x].
snoc :: List a n -> a -> List a (Succ n)
snoc Nil x = Cons x Nil
snoc (Cons x xs) y = Cons x (snoc xs y)


-- Appending two lists of length l and m, yields a list of length l+m.
-- 1. We need to find a representation for the sum of l and m.
-- 2. The user needs to implement append as well as providing a proof that the resulting length is l+m.
-- 3. The type checker will verify that the property "l+m" is satisfied.
--
-- The property "l+m" needs to be represented at the level of types.
-- For this purpose, we introduce the following data type.
data Sum x y z where
  Base :: Sum Zero x x
       -- Fact:
       --  0 + x     = x
  Step :: Sum x y z -> Sum (Succ x) y (Succ z)
       -- Rule:
       -- If x + y = z
       -- then (x+1) + y = (z+1)
       --
       -- The above rule is formulated inductively.


-- Insight: Proofs are programs.
-- Consider the property that 1 + 2 = 3
-- where the below program represents a proof for this property.
onePlusTwoEqualsThree :: Sum (Succ Zero) (Succ (Succ Zero)) (Succ (Succ (Succ Zero)))
onePlusTwoEqualsThree = Step Base


-- Let's consider the append function.
-- As an additional (first) argument we find a proof for the to be verified property ("l+m").
-- We make use of the proof during the construction of the program.
-- The type checker ensures that the program satisfies the property.
appendProp :: Sum l m n -> List a l -> List a m -> List a n
appendProp Base Nil xs = xs
appendProp (Step p) (Cons x xs) ys = Cons x (appendProp p xs ys)


example = appendProp onePlusTwoEqualsThree listNonEmpty1 listNonEmpty2


-- We make use of some Haskell extension to let the compiler
-- infer the proof of the "l+m" property for us.

type family Plus x y
type instance Plus Zero x = x
type instance Plus (Succ x) y = Succ (Plus x y)

-- The proof for the propery "l+m" is now implicit.
-- The compiler will carry out the proof steps for us
-- and insert the proof into the program text.
appendProp2 :: List a l -> List a m -> List a (Plus l m)
appendProp2 Nil xs = xs
appendProp2 (Cons x xs) ys = Cons x (appendProp2 xs ys)