https://qiita.com/as_capabl/items/2031fe28e577e77dc269 のサボってない版

siri_improved.hs

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE ConstraintKinds #-}

module Main where

import GHC.TypeLits (Nat, KnownNat)
import GHC.TypeLits.List (KnownNats, natsVal, NatList(..), natsList)
import Data.Proxy (Proxy(..))
import Control.Category (Category(..))
import Data.Singletons.Prelude.List ((:++))
import Data.Void (Void, absurd)
import Prelude hiding ((.), id)

-- しりとりの圏(単相)
data Siri (xs :: [Nat]) (a :: Nat) (b :: Nat) where
  SiriUnit :: Proxy a -> Siri '[a] a a
  SiriCons :: Proxy a -> (Siri ys b c) -> Siri (a ': ys) a c

-- 射の合成
siriConcat :: Siri xs a b -> Siri xs' b c -> Siri (xs :++ xs') a c
siriConcat (SiriUnit proxy) ks = SiriCons proxy ks
siriConcat (SiriCons proxy ks) ks' = SiriCons proxy (ks `siriConcat` ks')

-- 射を文字列に
showSiri :: KnownNats xs => Siri xs a b -> String
showSiri (_ :: Siri xs a b) = map (toEnum . fromEnum) $ natsVal (Proxy @xs)

-- しりとりの圏 (全体)
data AllSiri' idtype a b where
  AllSiriId :: idtype -> AllSiri' idtype a a
  AllSiriContent :: KnownNats xs => Siri xs a b -> AllSiri' idtype a b

type AllSiri = AllSiri' ()
addId :: AllSiri' Void a b -> AllSiri a b
addId (AllSiriId v) = absurd v
addId (AllSiriContent x) = AllSiriContent x

-- 射を文字列に
showAllSiri :: KnownNat a => AllSiri a b -> String
showAllSiri (AllSiriId () :: AllSiri a b) = showSiri (SiriUnit (Proxy @a))
showAllSiri (AllSiriContent k) = showSiri k

-- 圏のインスタンス
instance Category AllSiri where
  id = AllSiriId ()
  f . g = g `allSiriConcat` f

allSiriConcat :: AllSiri a b -> AllSiri b c -> AllSiri a c
allSiriConcat (AllSiriId ()) k = k
allSiriConcat (AllSiriContent c) k = addId $ prependToAllSiri natsList c k

prependToAllSiri :: KnownNats xs => NatList xs -> Siri xs a c -> AllSiri c b -> AllSiri' Void a b
prependToAllSiri _ x (AllSiriId ()) = AllSiriContent x
prependToAllSiri _ (SiriUnit _) (AllSiriContent x) = AllSiriContent x
prependToAllSiri (pr' :<# ns) (SiriCons _ x :: Siri xs a c) k =
  case prependToAllSiri ns x k of
    AllSiriId v -> absurd v
    AllSiriContent k' -> AllSiriContent (SiriCons pr' k')

-- 使用例
main :: IO ()
main = do
  let はすけるびー = るびー . はすける
      -- これはだめ = はすける . るびー
  putStrLn $ showAllSiri はすけるびー
  putStrLn $ showAllSiri (はすけるびー . id)
  putStrLn $ showAllSiri (id . はすけるびー)

はすける = AllSiriContent はすける'
はすける' = SiriCons (Proxy @12399)
         $ SiriCons (Proxy @12377)
         $ SiriCons (Proxy @12369)
         $ SiriUnit (Proxy @12427)

るびー = AllSiriContent るびー'
るびー' = SiriCons (Proxy @12427)
       $ SiriCons (Proxy @12403)
       $ SiriUnit (Proxy @12540)