Created
December 7, 2017 08:47
-
-
Save as-capabl/215784db6fc8e0c2d6fbe51325b5b162 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# 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