{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}

-- https://blog.jle.im/entry/fixed-length-vector-types-in-haskell-2015.html

module Types where

-- Nat is a type of a set of types here (thanks to DataKinds extension
-- ie, constructors of `Nat' are types. Not values
-- :k
data Nat
  = Z
  | S Nat
--deriving Show
-- ghci> :k Nat
-- Nat :: *
-- ghci> :k Z
-- Z :: Nat
-- ghci> :k S
-- S :: Nat -> Nat
-- ghci> :k 'S
-- 'S :: Nat -> Nat


data Vec :: Nat -> * -> * where
  Nil :: Vec 'Z a
  (:>) :: a -> Vec n a -> Vec ('S n) a

infixr 5 :>
deriving instance Show a => Show (Vec n a)
deriving instance Eq a => Eq (Vec n a)

hd :: Vec ('S n) a -> a  
hd (x :> _) = x

-- λ> hd (1 :> 2 :> Nil)
-- 1
-- λ> hd (Nil)
--  * Couldn't match type 'Z with 'S n0
--    Expected: Vec ('S n0) a
--      Actual: Vec 'Z a
--  * In the first argument of `hd', namely `(Nil)'
--    In the expression: hd (Nil)
--    In an equation for `it': it = hd (Nil)


tl :: Vec ('S n) a -> Vec n a
tl (_ :> xs) = xs

-- tl (1 :> 2 :> Nil) :: Num a => Vec ('S 'Z) a
-- λ> :t tl
-- tl :: Vec ('S n) a -> Vec n a
-- λ> tl (1 :> Nil)
-- tl (1 :> Nil) :: Num a => Vec 'Z a


-- https://downloads.haskell.org/ghc/latest/docs/users_guide/exts/type_families.html#extension-TypeFamilies 

-- Addition at type level
type family (+) (x :: Nat) (y :: Nat) where
  'Z + y = y
  --x + 'Z = x -- not in blog post
  ('S x) + y = 'S (x + y)

-- Addition for values of the `Nat' type
(+>) :: Nat -> Nat -> Nat
Z +> y = y
(S x) +> (S y) = S (x +> y)

append :: Vec n a -> Vec m a -> Vec (n + m) a
append (x :> v1') v2 = x :> (append v1' v2)
append Nil v2 = v2
--append v1 Nil = v1  -- not in blog post

-- λ> append (1 :> 2 :> Nil) (3 :> 4 :> 5 :> Nil)
-- append (1 :> 2 :> Nil) (3 :> 4 :> 5 :> Nil)
--   :: Num a => Vec ('S ('S ('S ('S ('S 'Z))))) a

-- --After giving Show
-- λ> append (1 :> 2 :> Nil) (3 :> 4 :> 5 :> Nil)
-- 1 :> (2 :> (3 :> (4 :> (5 :> Nil))))