昨日のズンドコネタの (多分) 型レベル版

zndk-kiyoshi-typelevel.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE FlexibleContexts #-}

module Lib where

import GHC.TypeLits
import Data.Proxy

data List :: * -> * where
    Nil   :: List a
    (:::) :: a -> List a -> List a

deriving instance Show a => Show (List a)

infixr 5 :::

data ZnDk = Kiyoshi | NonKiyoshi

class ShowZnDk (z :: ZnDk) where
    showZnDk :: Proxy z -> String

instance ShowZnDk Kiyoshi    where showZnDk _ = "き・よ・し！"
instance ShowZnDk NonKiyoshi where showZnDk _ = "きよしじゃない"

type family ToZnDk (l :: List a) :: ZnDk where
    ToZnDk Nil = NonKiyoshi
    ToZnDk ("ズン" ::: "ズン" ::: "ズン" ::: "ズン" ::: "ドコ" ::: Nil) = Kiyoshi
    ToZnDk (_ ::: xs) = ToZnDk xs

kiyoshi :: (ShowZnDk (ToZnDk l)) => Proxy (l :: List a) -> String
kiyoshi (Proxy :: Proxy a) = showZnDk (Proxy :: Proxy (ToZnDk a))

test :: IO ()
test = do
    let p0 = Proxy :: Proxy Nil
    let p1 = Proxy :: Proxy ("ズン" ::: Nil)
    let p2 = Proxy :: Proxy ("ズン" ::: "ドコ" ::: Nil)
    let p3 = Proxy :: Proxy ("ズン" ::: "ズン" ::: "ズン" ::: "ドコ" :::  Nil)
    let p4 = Proxy :: Proxy ("ズン" ::: "ドコ" ::: "ズン" ::: Nil)
    let p5 = Proxy :: Proxy ("ズン" ::: "ズン" ::: "ズン" ::: "ズン" ::: "ズン" ::: "ドコ" :::  Nil)
    let p6 = Proxy :: Proxy ("ドコ" ::: "ズン" ::: "ズン" ::: "ズン" ::: "ズン" ::: "ドコ" :::  Nil)
    let p7 = Proxy :: Proxy ("ズン" ::: "ズン" ::: "ズン" ::: "ズン" ::: "ドコ" :::  Nil)
    putStrLn $ kiyoshi p0
    putStrLn $ kiyoshi p1
    putStrLn $ kiyoshi p2
    putStrLn $ kiyoshi p3
    putStrLn $ kiyoshi p4
    putStrLn $ kiyoshi p5
    putStrLn $ kiyoshi p6
    putStrLn $ kiyoshi p7

実行結果

$ stack exec typed-zndk-kiyoshi-exe
きよしじゃない
きよしじゃない
きよしじゃない
きよしじゃない
きよしじゃない
き・よ・し！
き・よ・し！
き・よ・し！