SHamburger (Space Space Space Space)
SHamburger (Cheese Space Space Space)
SHamburger (Cheese Tomato Space Space)
SHamburger (Cheese Tomato Meet Space)
SHamburger (Cheese Tomato Meet Ushi)

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}

module Hamberger where

import Hamburger.TH (defineInstances)

-- | A kind of the topping, and types.
data Topping = Space -- ^ Mean a space, it can be inserted some @Topping@
             | Cheese | Tomato | Meet | Ushi

-- |
-- A type level function
-- that maps @HamburgerT@ and @Topping@ to @HamburgerT@.
--
-- If @HamburgerC a b c d@ :: @HamburgerT@ of the domain has no space, or @Fail@ is specified to the domain,
-- return @Fail@ type.
type family AddTopping (h :: HamburgerT) (t :: Topping) :: HamburgerT where
  AddTopping (HamburgerC Space b c d) t = HamburgerC t b c d
  AddTopping (HamburgerC a Space c d) t = HamburgerC a t c d
  AddTopping (HamburgerC a b Space d) t = HamburgerC a b t d
  AddTopping (HamburgerC a b c Space) t = HamburgerC a b c t
  AddTopping _ _ = Fail

-- | A kind of the abstract hamburger
data HamburgerT = HamburgerC Topping Topping Topping Topping -- ^ A type constructor of the abstract hamburger
                | Fail -- ^ Mean a fail of a mapping of @AddTopping@


{- The dependent type -}

-- |
-- A concrete of the hamburger
-- (A type constructor for a type of @HamburgerT@ kind).
data SHamburger (h :: HamburgerT) where
  Concrete :: STopping -> STopping -> STopping -> STopping -> SHamburger (HamburgerC a b c d :: HamburgerT)

-- | A singleton type for @Topping@ kind.
data STopping = SSpace | SCheese | STomato | SMeet | SUshi
  deriving (Show)

-- | Represent the simply dependent type
class Singleton (h :: HamburgerT) where
  sing :: SHamburger h


-- Define any instances for 126 patterns !
defineInstances


type BasicHamburgerC = HamburgerC Space Space Space Space

type HamburgerC1 = AddTopping BasicHamburgerC Cheese -- these kind is @HamburgerT@
type HamburgerC2 = AddTopping HamburgerC1 Tomato
type HamburgerC3 = AddTopping HamburgerC2 Meet
type HamburgerC4 = AddTopping HamburgerC3 Ushi
type HamburgerC5 = AddTopping HamburgerC4 Ushi -- = Fail

x0 = sing :: SHamburger BasicHamburgerC
x1 = sing :: SHamburger HamburgerC1
x2 = sing :: SHamburger HamburgerC2
x3 = sing :: SHamburger HamburgerC3
x4 = sing :: SHamburger HamburgerC4
--x5 = sing :: SHamburger HamburgerC5 -- This is the compile error because Refl is not a Fail's value


main :: IO ()
main = do
  print x0
  print x1
  print x2
  print x3
  print x4

{-# LANGUAGE TemplateHaskell #-}

module Hamburger.TH where

import Language.Haskell.TH (Type(..), Name, mkName, Exp(..), DecsQ, Dec(..), Clause(..), Pat(..), Body(..), Lit(..))

type TypeName = String

type Topping4 = (TypeName, TypeName, TypeName, TypeName)


topping4s :: [Topping4]
topping4s = [(w, x, y, z) | w <- toppings, x <- toppings, y <- toppings, z <- toppings]
  where
    toppings :: [TypeName]
    toppings = ["Space", "Cheese", "Tomato", "Meet", "Ushi"]

-- | Make a AST of @Type@ is like "(HamburgerC Space Cheese Tomato Meet)"
hamburgerC :: Topping4 -> Type
hamburgerC (w, x, y, z) = ParensT (ConT (mkName "HamburgerC") 
                            `AppT` ConT (mkName w)
                            `AppT` ConT (mkName x)
                            `AppT` ConT (mkName y)
                            `AppT` ConT (mkName z))

-- |
-- Make a AST of @Exp@ is like "Concrete SSpace SCheese STomato SMeet"
-- (@Topping4@ elements are added "S" prefix for @STopping@).
concrete :: Topping4 -> Exp
concrete (w, x, y, z) = ConE (mkName "Concrete")
                 `AppE` ConE (mkName $ "S" ++ w)
                 `AppE` ConE (mkName $ "S" ++ x)
                 `AppE` ConE (mkName $ "S" ++ y)
                 `AppE` ConE (mkName $ "S" ++ z)


-- | Define @Singleton@ instances and @Show@ instances for any pattern of @topping4@
defineInstances :: DecsQ
defineInstances = do
  let singletonInstances = map defineSingletonInstance topping4s
      showInstances      = map defineShowInstance topping4s
  return $ singletonInstances ++ showInstances
  where
    defineSingletonInstance :: Topping4 -> Dec
    defineSingletonInstance t4@(w, x, y, z) =
      InstanceD Nothing []
        (ConT (mkName "Singleton") `AppT` hamburgerC t4)
        [
          FunD (mkName "sing") [Clause [] (NormalB $ concrete t4) []]
        ]

    defineShowInstance :: Topping4 -> Dec
    defineShowInstance t4@(w, x, y, z) =
      InstanceD Nothing []
        (ConT (mkName "Show") `AppT` ParensT (ConT (mkName "SHamburger") `AppT` hamburgerC t4))
        [
          FunD (mkName "show") [Clause [WildP] (NormalB $
              (LitE . StringL $ "SHamburger (" ++ w ++ " " ++ x ++ " " ++ y ++ " " ++ z ++ ")")
          ) []]
        ]

type family AddTopping (h :: HamburgerT) (t :: Topping) :: HamburgerT where
  AddTopping (HamburgerC Space b c d) t = HamburgerC t b c d
  AddTopping (HamburgerC a Space c d) t = HamburgerC a t c d
  AddTopping (HamburgerC a b Space d) t = HamburgerC a b t d
  AddTopping (HamburgerC a b c Space) t = HamburgerC a b c t
  AddTopping _ _ = Fail

data SHamburger (h :: HamburgerT) where
  Concrete :: STopping -> STopping -> STopping -> STopping -> SHamburger (HamburgerC a b c d :: HamburgerT)

data STopping = SSpace | SCheese | STomato | SMeet | SUshi
  deriving (Show)

instance Singleton (HamburgerC Cheese Ushi Meet Space) where
  sing = Concrete SCheese SUshi SMeet SSpace

型レベル: HamburgerC Cheese Ushi Meet Space
値レベル: Concrete SCheese SUshi SMeet SSpace