しりとりの話

Main.hs

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DataKinds #-}
module Main where

import Prelude hiding ((.), Word)
import qualified Prelude
import Data.Singletons
import Data.Singletons.TH
import Data.Singletons.TypeLits
import Data.Singletons.Prelude.Eq
import Data.Singletons.Prelude.List
import Data.Kind
import Data.Type.Equality
import Control.Category

-- このあたりの
-- http://d.hatena.ne.jp/m-hiyama/20060821/1156120185
-- https://qiita.com/hiratara/items/6265b5d4791144bee33b
-- https://qiita.com/as_capabl/items/2031fe28e577e77dc269
main :: IO ()
main = do
  -- 静的に利用する例
  -- print (はすける . るびー) -- 型エラー
  print (るびー . はすける) -- OK

  -- 与えられた文字列から動的にWord ns型を作るもの
  withThisWord' "与えられた" print
  withThisWord' "文字列" print

  -- 動的に利用する例
  withThisWord' "はすける" $ \haskell ->
    withThisWord' "るびー" $ \ruby -> do

      let はすける' = WFTLift haskell
          るびー' = WFTLift ruby

      -- ここで はすける' の型は はすける の型と同じ
      -- ここで るびー' の型は るびー の型と同じ

      -- でも，それはwithThisWord'を適用する文字列によって変わってしまうため，
      -- 素直に次のしりとり合成を行うことはできない．

      -- print (るびー' . はすける') -- 型エラー

      -- ruby側の最初の文字の型と，haskell側の文字の型を比べて，
      -- 同じだったときのルートと違ったときのルートを作る必要がある
      case sLast (wordToSing haskell) `testEquality` sHead (wordToSing ruby) of
        Nothing   -> do
          -- 違ったとき，合成可能な要件を満たさないので，
          -- こちらの分岐では型が合わずに合成できない

          -- print (るびー' . はすける') -- 型エラー

          putStrLn "error: 合成できませんでした"
        Just Refl -> do
          -- 対して，こちらの分岐では，
          -- 型検査器が合成可能であることを理解している．
          -- これまで他の場所では型エラーになっていたのと全く同じ式だが，
          -- このマッチのスコープ内でのみ型エラーにならず合成できる．

          print (るびー' . はすける') -- OK


  -- 実際，上記と同じ処理を，
  -- 次のようにしりとり合成できない文字列に適用しても合成はできない
  withThisWord' "はすけろ" $ \haskell ->
    withThisWord' "るびー" $ \ruby -> do
      let はすけろ' = WFTLift haskell
          るびー' = WFTLift ruby
      case sLast (wordToSing haskell) `testEquality` sHead (wordToSing ruby) of
        Nothing   -> putStrLn "error: 合成できませんでした"
        Just Refl -> print (るびー' . はすけろ') -- OK

  -- 実行時に失敗するルートがあるように挙動が動的に見えるので，
  -- 処理としては

  -- if last "はすける" == head "るびー"
  --   then compose "はすける" "るびー" -- 合成する
  --   else error ... -- 合成できない

  -- と，同じじゃないかと感じるかもしれないが，
  -- 型検査器が合成可能であると理解したスコープ以下でしか，
  -- しりとり合成(.)が行えないというのが「安全」


data Word :: [Nat] -> * where
  WUnit :: Sing n -> Word '[n]
  WCons :: Sing n -> Word ns -> Word (n ': ns)

instance Show (Word ns) where
  show (WUnit n) = [toEnum $ fromEnum $ fromSing n]
  show (WCons n ns) = toEnum (fromEnum $ fromSing n) : show ns

wordToSing :: Word ns -> Sing ns
wordToSing (WUnit ns) = SCons ns sing
wordToSing (WCons n ns) = SCons n (wordToSing ns)

data SomeWord where SomeWord :: Word ns -> SomeWord

withSomeWord :: SomeWord -> (forall (ns :: [Nat]) . Word ns -> a) -> a
withSomeWord (SomeWord w) f = f w

strToSomeWord :: String -> Maybe SomeWord
strToSomeWord = go Prelude.. map (toEnum Prelude.. fromEnum) where
  go [] = Nothing
  go [n] = withSomeSing n $ \sn -> Just (SomeWord (WUnit sn))
  go (n:ns@(_:_)) = case go ns of
    Nothing -> Nothing
    Just sw -> withSomeWord sw $ \wns ->
      withSomeSing n $ \sn -> Just $ SomeWord $ WCons sn $ wns

withThisWord :: String -> (String -> a) -> (forall (ns :: [Nat]) . Word ns -> a) -> a
withThisWord s d f = case strToSomeWord s of
  Nothing -> d s
  Just sw -> withSomeWord sw f

withThisWord' :: String -> (forall (ns :: [Nat]) . Word ns -> a) -> a
withThisWord' s f = withThisWord s error f

data WordFromTo :: Nat -> Nat -> * where
  WFTId   :: WordFromTo a a
  WFTLift :: Word ns -> WordFromTo (Head ns) (Last ns)
  WFTJoin :: WordFromTo a b -> WordFromTo b c -> WordFromTo a c

instance Category WordFromTo where
  id = WFTId
  WFTId . g = g
  f . WFTId = f
  f . g = WFTJoin g f

instance Show (WordFromTo a b) where
  show WFTId = ""
  show (WFTLift w) = show w
  show (WFTJoin a b) = show a ++ drop 1 (show b)

はすける :: WordFromTo 12399 12427
はすける = WFTLift go where
  go = WCons (sing :: Sing 12399)
     $ WCons (sing :: Sing 12377)
     $ WCons (sing :: Sing 12369)
     $ WUnit (sing :: Sing 12427)

るびー :: WordFromTo 12427 12540
るびー = WFTLift go where
  go = WCons (sing :: Sing 12427)
     $ WCons (sing :: Sing 12403)
     $ WUnit (sing :: Sing 12540)