BasicTypeLevel.hs

-- Code from the blog post "Basic Type Level Programming" by Matt Parsons
-- http://www.parsonsmatt.org/2017/04/26/basic_type_level_programming_in_haskell.html
--
-- References https://www.schoolofhaskell.com/user/konn/prove-your-haskell-for-great-safety/dependent-types-in-haskell

{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}

-- NATURALS / PEANO ARITHMITIC

data Nat = Zero | Succ Nat
-- We se the single-quote style to delineate type vs. term levels. 
data Vector n a where
    VNil :: Vector 'Zero a
    VCons :: a -> Vector n a -> Vector ('Succ n) a
   
instance Show a => Show (Vector n a) where
    show VNil         = "VNil"
    show (VCons a as) = "VCons " ++ show a ++ " (" ++ show as ++ ")"

-- Open type family, as opposed to a closed one which simply means it's embedded in a typeclass. 
--
-- First implementation, to be contrasted against final.
--type family Add x y where
--    Add 'Zero n = n
--    Add ('Succ n) m = Add n ('Succ m)
--
-- Final implementation.
type family Add x y where
    Add 'Zero n = n
    Add ('Succ n) m = 'Succ (Add n m)

append :: Vector n a -> Vector m a -> Vector (Add n m) a
append VNil xs           = xs
append (VCons a rest) xs = VCons a (append rest xs)


-- HETEROGENOUS LISTS

data HList xs where
    HNil :: HList '[]
    (:::) :: a -> HList as -> HList (a ': as)

infixr 6 :::

instance Show (HList '[]) where
    show HNil = "HNil"
    
instance (Show (HList as), Show a) 
    => Show (HList (a ': as)) where
    show (a ::: rest) = 
        show a ++ " ::: " ++ show rest
        
 -- EXTENSIBLE RECORDS
 
 newtype s >> a = Named a

data HRec xs where
    HEmpty :: Hrec '[]
    HCons :: (s >> a) -> HRec xs -> Hrec (s >> a ': xs)
    
instance Show (HRec '[]) where
    show _ = "HEmpty"
                
instance (Show a, KnownSymbol s, Show (HRec xs)) 
    => Show (HRec (s >> a ': xs)) where
    show (HCons (Named a) rest) =
        let val = show a
            key = symbolVal (undefined :: x s)
            more = show rest
         in "(" ++ key ++ ": " ++ val ++ ") " ++ more
            
topLevelFunction :: a0 -> (a0 -> b0) -> b0
topLevelFunction a = go
  where
    go :: (a1 -> b1) -> b1
    go f = f a

{-
Exercise:
Write an Aeson ToJSON instance for this HRec type which converts into a JSON object.

Bonus exercise: 
Write an Aeson FromJSON instance for the HRec type.
-}