型レベルでのL-systemのようなもの

type_L_system.hs

{-# LANGUAGE DataKinds, UndecidableInstances, FlexibleInstances #-}
{-# LANGUAGE TypeFamilies, TypeOperators, ScopedTypeVariables #-}
{-# LANGUAGE PolyKinds #-}

data V = A | B deriving Show

type Omega = '[A]

type family P (v :: V) :: [V]
type instance P A = '[B]
type instance P B = '[A,B]

type family (xs :: [a]) ++ (ys :: [a]) :: [a]
type instance '[] ++ ys = ys
type instance (x ': xs) ++ ys = x ': (xs ++ ys)

type family Foo (xs :: [V]) :: [V]
type instance Foo '[] = '[]
type instance Foo (x ': xs) = P x ++ Foo xs

data Nat = Z | S Nat

type family Bar (xs :: [V]) (n :: Nat) :: [V]
type instance Bar xs Z = xs
type instance Bar xs (S n) = Bar (Foo xs) n

type family Baz (n :: Nat) :: [V]
type instance Baz n = Bar Omega n

type family Bar' (xs :: [V]) (n :: Nat) :: [[V]]
type instance Bar' xs Z = '[xs]
type instance Bar' xs (S n) = xs ': Bar' (Foo xs) n

type family Baz' (n :: Nat) :: [[V]]
type instance Baz' n = Bar' Omega n

class Value (v :: [V]) where
    toVal :: Result v -> [V]
instance Value '[] where
    toVal _ = []
instance Value xs => Value (A ': xs) where
    toVal _ = A : toVal (Result :: Result xs)
instance Value xs => Value (B ': xs) where
    toVal _ = B : toVal (Result :: Result xs)

data Result (v :: [V]) = Result
result :: Result (Baz (S (S (S Z))))
result = Result

class Value' (v :: [[V]]) where
    toVal' :: Result' v -> [[V]]
instance Value' '[] where
    toVal' _ = []
instance (Value x, Value' xs) => Value' (x ': xs) where
    toVal' _ = toVal (Result :: Result x) : toVal' (Result' :: Result' xs)

data Result' (v :: [[V]]) = Result'
result' :: Result' (Baz' (S (S (S (S (S Z))))))
result' = Result'