Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
{-# 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)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.