LoginSignup
1
1

More than 3 years have passed since last update.

@matoruru

Symbolのすごく簡単な具体例をひとつ（＋解説）

Last updated at Posted at 2019-10-20

はじめに

前回はRowToListについての簡単記事を書きました。続きというわけではないですが、同じような構成の記事を書いてみます。

目的

Symbolの文字列（5文字）を逆順にしたい("ABCDE"から"EDCBA"、など)。

今回は簡単な具体例ということで、文字列の長さは5文字固定にします。こういうものには再帰を使った例が多い気がするのですが、ここでは再帰を使っていません。再帰を使わない本記事の方法では文字数の固定やコード量の増加など不都合なことは多いですが、今回はあくまでSymbolの例として分かりやすいことを重視しているので、気にせず！(記事の最後におまけとして再帰を使った改善例を載せています)

基礎知識

ここは飛ばしてもいいかもしれません。興味がある方はぜひ読んでみてください！

Symbolはtype(型)ではなくkind(種)なので、そのまま型として使うことができません。

型はIntやString、Array a、Maybe aなどで（ここでArrayとMaybeは型をもらって型を返す型コンストラクタです。Array Intなど。）、関数や値の型を明示するときに「::」の右側に書くことのできるものです。

func1 :: Int -> Int
func1 a = a

func2 :: Array Int -> String
func2 _ = "atai wo mushi shitemasu."

func3 :: Maybe Int -> Int
func3 (Just v) = (v :: Int)  -- 書く必要ない 
func3 Nothing  = (0 :: Int)  -- ですが、一例です

対して、種であるSymbolでは例えば、以下のようなことができません。

func :: "This is a symbol" -> Int
func _ = 1

-- こんなエラーが出ます
-- [PureScript Kinds DoNotUnify] [E]  Could not match kind
--
--    Type
--  with kind
--    Symbol

型が書かれるべき場所に種を書いてしまったので、エラーになってしまいました。Intに対する1、Array Stringに対する["a", "b"]、Maybe Intに対するJust 2、などのように、その型に属する値を作ることが種の場合はできません。

ここで、代数的データ型の宣言方法を見てみましょう。

-- MyType1型の値としてNeko、Hello、Oyatsu、Matoruruが存在する
data MyType1 = Neko | Hello | Oyatsu | Matoruru

-- MyType2 a型の値としてInu a、Dog、B aが存在する
data MyType2 a = Inu a | Dog | B a

これらはこんなふうに使えます。

func1 :: MyType1
func1 = Neko

func2 :: MyType1 -> MyType2 Int
func2 _ = Inu 2

func3 :: MyType1 -> MyType2 String
func3 _ = Dog

func4 :: MyType2 String
func4 = func3 $ Oyatsu

結構重要なのがMyType2 a型のDogですが、これはMyType2 Int型でもMyType2 String型でもMyTpe2 (Array Int)型でも、見た目は同じDogとして型情報を隠し持っています。Maybe a型のNothingとか、Array a型の[]とかもそれです。

func1 :: MyType2 String
func1 = Dog

func2 :: MyType2 (Array Int)
func2 = Dog

func3 :: MyType2 String
func3 = func1

func4 :: MyType2 String
func4 = func2 -- 見た目は同じDogなのに、これはできない！

見た目は同じでも、型情報を持つことができるということです。同じような宣言方法で、代数的データ型は種であるSymbolを受け取って型を作ることができます。

data MyType3 (sym :: Symbol) = Meow

-- symは型ではないので、これはできない
data MyType4 (sym :: Symbol) = Meoww sym

さっきのMyType2の例と同じようなことをしてみましょう。

func1 :: MyType3 "ohayo!"
func1 = Meow

func2 :: MyType3 "hajimemashite"
func2 = Meow

func3 :: MyType3 "ohayo!"
func3 = func1

func4 :: MyType3 "ohayo!"
func4 = func2 -- 見た目は同じMeowなのに、これはできない！

つまり、そのままでは型の世界に存在できない種の情報を持ち、型引数を通して種を受け渡しできる値が作れたということです。

このような型と値はよくProxyという名前で使われます。種SymbolのProxyはSProxy、種NatのProxyはNProxyとか、そのような名付け方をされます。

以下のように書きます。

data SProxy (sym :: Symbol) = SProxy

先程の例で出したMyType3型と同じ形式ですね。

せっかく作りましたが、SProxyは既にPursuitにあります。

本題に戻ります。

具体例

Main.purs
module Main where

import Prim.Symbol as Symbol
import Type.Prelude (SProxy(..))

class Cons5
  (s1 :: Symbol)
  (s2 :: Symbol)
  (s3 :: Symbol)
  (s4 :: Symbol)
  (s5 :: Symbol)
  (sym :: Symbol)
  | s1 s2 s3 s4 s5 -> sym
  , sym -> s1 s2 s3 s4 s5

instance cons5 ::
  ( Symbol.Cons s1 t1 sym
  , Symbol.Cons s2 t2 t1
  , Symbol.Cons s3 t3 t2
  , Symbol.Cons s4 t4 t3
  , Symbol.Cons s5 t5 t4
  ) => Cons5 s1 s2 s3 s4 s5 sym

class Reverse (original :: Symbol) (reversed :: Symbol) | original -> reversed

instance reverse ::
  ( Cons5 s1 s2 s3 s4 s5 original
  , Cons5 s5 s4 s3 s2 s1 reversed
  ) => Reverse original reversed

test1 :: SProxy "EDCBA"
test1 = SProxy :: forall output. Reverse "ABCDE" output => SProxy output

test2 :: SProxy "ABCDE"
test2 = SProxy :: forall output. Reverse "EDCBA" output => SProxy output

test3 :: SProxy "NEKO!"
test3 = SProxy :: forall output. Reverse "!OKEN" output => SProxy output

test1、test2、test3では目的の型(元のSymbol文字列が逆順になっているもの)がうまく導出されたかどうかを確かめています。

型クラスReverseとCons5は、Symbolを変換する関数のように動作します。

Reverseは、型引数originalとして受け取ったSymbolを逆順に並べ替え、それを型引数reversedにします。内部でCons5を使います。

Cons5には2つの役割があり、1つ目はsymとして受け取ったSymbolをs1、s2、s3、s4、s5に分解すること、2つ目はその逆でs1、s2、s3、s4、s5として受け取ったSymbolを結合してsymにすることです。

順番に見る＋解説

少しずつ増やしながら見ていきます。

1. Symbolを分解する型クラスCons5を用意する

Cons型クラスは、Cons a b cのとき、cに受け取ったSymbolの1文字目をa、それ以降をbにします。また逆に、aに受け取った1文字とbに受け取った数文字を結合したものをcにすることもできます。例えば、Cons "N" "eko" "Neko"です。Cons a b "Neko"のとき、aは"N"、bは"eko"になります。

この知識で、以下のCons5型クラスとインスタンスの宣言が読めます。

class Cons5
  (s1 :: Symbol)
  (s2 :: Symbol)
  (s3 :: Symbol)
  (s4 :: Symbol)
  (s5 :: Symbol)
  (sym :: Symbol)
  | s1 s2 s3 s4 s5 -> sym
  , sym -> s1 s2 s3 s4 s5

instance cons5 ::
  ( Symbol.Cons s1 t1 sym
  , Symbol.Cons s2 t2 t1
  , Symbol.Cons s3 t3 t2
  , Symbol.Cons s4 t4 t3
  , Symbol.Cons s5 t5 t4
  ) => Cons5 s1 s2 s3 s4 s5 sym

Cons5は、6個の型引数を持ち、受け取った5つのSymbolを結合してsymにするか、symを5つに分解することができます。実際の動作はインスタンスの型制約に書いてあります。

まず、symに"Hello"を受け取ったとして、分解の方から見ていきます。

  1. symが"Hello"なので、Consによりs1が"H"、t1が"ello"だとわかる。
  2. t1が"ello"なので、Consによりs2が"e"、t2が"llo"だとわかる。
  3. t2が"llo"なので、Consによりs3が"l"、t3が"lo"だとわかる。
  4. t3が"lo"なので、Consによりs4が"l"、t4が"o"だとわかる。
  5. t4が"o"なので、Consによりs5が"o"、t5が""だとわかる。
  6. 以上をまとめて、Cons5 s1 s2 s3 s4 s5 symはCons5 "H" "e" "l" "l" "o" "Hello"だとわかる。

結合ではこの逆のことが行われます。この場合はSymbol.Cons s5 t5 t4のt5がわからないままですが、最終的にはつじつま合わせで空白だったことにしてくれます。つじつま合わせのために、型注釈が必要になります。型注釈が間違っている場合は型エラーを出して知らせてくれます(正しくするまでコンパイルできない)。

2. Symbolを逆順にする型クラスReverseを用意する

class Cons5
  (s1 :: Symbol)
  (s2 :: Symbol)
  (s3 :: Symbol)
  (s4 :: Symbol)
  (s5 :: Symbol)
  (sym :: Symbol)
  | s1 s2 s3 s4 s5 -> sym
  , sym -> s1 s2 s3 s4 s5

instance cons5 ::
  ( Symbol.Cons s1 t1 sym
  , Symbol.Cons s2 t2 t1
  , Symbol.Cons s3 t3 t2
  , Symbol.Cons s4 t4 t3
  , Symbol.Cons s5 t5 t4
  ) => Cons5 s1 s2 s3 s4 s5 sym

class Reverse (original :: Symbol) (reversed :: Symbol) | original -> reversed

instance reverse ::
  ( Cons5 s1 s2 s3 s4 s5 original
  , Cons5 s5 s4 s3 s2 s1 reversed
  ) => Reverse original reversed

Reverse型クラスのインスタンスの中で、1. で用意したCons5を使っています。Reverseは|の横に書かれた関数従属性(functional dependency)original -> reversedにより、originalからreversedを導出できることがわかります。

forall output. Reverse "Hello" outputのように型クラスが使われた場面を考えます。

  1. Reverse "Hello" reversedとして型引数originalのSymbolが決まる。
  2. originalが"Hello"であることがわかっているので、Cons5 s1 s2 s3 s4 s5 originalはCons5 s1 s2 s3 s4 s5 "Hello"になることがわかる。
  3. Cons5型クラスはsymに渡されたSymbolをs1、s2、s3、s4、s5に分解できるので、Cons5 s1 s2 s3 s4 s5 "Hello"はCons5 "H" "e" "l" "l" "o" "Hello"になることがわかる。
  4. 次のCons5ではs5〜s1はわかっているので、5文字を結合してreversedを導出できる。上のCons5と下のCons5では分解された各Symbolを逆順に並べているので、Cons5 "o" "l" "l" "e" "H" reversedとなる。ここから、Cons5 "o" "l" "l" "e" "H" "olleH"と、reversedが"olleH"であることがわかる。
  5. Reverse "Hello" reversedはReverse "Hello" "olleH"であることがわかった。
  6. forall output. Reverse "Hello" outputのoutputが"olleH"になることがわかる。

ここまでで、ある5文字のSymbol文字列から逆順を導出できるようになりました！

型クラスReverseを試してみる

実際にtest1関数の中で、Reverseで導出された逆順のSymbolをSProxyに渡して型を作ってみます。

class Cons5
  (s1 :: Symbol)
  (s2 :: Symbol)
  (s3 :: Symbol)
  (s4 :: Symbol)
  (s5 :: Symbol)
  (sym :: Symbol)
  | s1 s2 s3 s4 s5 -> sym
  , sym -> s1 s2 s3 s4 s5

instance cons5 ::
  ( Symbol.Cons s1 t1 sym
  , Symbol.Cons s2 t2 t1
  , Symbol.Cons s3 t3 t2
  , Symbol.Cons s4 t4 t3
  , Symbol.Cons s5 t5 t4
  ) => Cons5 s1 s2 s3 s4 s5 sym

class Reverse (original :: Symbol) (reversed :: Symbol) | original -> reversed

instance reverse ::
  ( Cons5 s1 s2 s3 s4 s5 original
  , Cons5 s5 s4 s3 s2 s1 reversed
  ) => Reverse original reversed

test1 :: SProxy "EDCBA"
test1 = SProxy :: forall output. Reverse "ABCDE" output => SProxy output
  1. の説明に従うと、forall output. Reverse "ABCDE" outputのoutputはEDCBAになることがわかります。ここで求めた逆順のSymbolをSProxyに渡したものをSProxyの型注釈に書きます。
test1 = SProxy :: forall output. Reverse "ABCDE" output => SProxy output

の部分です。型注釈をまとめると、SProxy :: SProxy outputがSProxy :: SProxy "EDCBA"になるので、test1関数の型定義にはtest1 :: SProxy "EDCBA"と書けます。

次の例でも同じです。

test2 :: SProxy "ABCDE"
test2 = SProxy :: forall output. Reverse "EDCBA" output => SProxy output

test3 :: SProxy "NEKO!"
test3 = SProxy :: forall output. Reverse "!OKEN" output => SProxy output

おまけ

簡単な例として再帰を使わないものを見せたかったので上記のようにしていましたが、拡張性を考えると再帰定義を使って簡潔にしたほうがいいです。Symbolの文字数制限もありません(長すぎると再帰の途中でコンパイラが諦めてしまうため実際には制限なしとはいきませんが…)。

以下のようにするとうまくできます。

module Main where

import Prim.Symbol as Symbol
import Type.Prelude (SProxy(..))

class Reverse (original :: Symbol) (reversed :: Symbol) | original -> reversed
                                                        , reversed -> original

instance reverseNil :: Reverse "" ""

else instance reverse ::
  ( Symbol.Cons s t original
  , Reverse t r
  , Symbol.Append r s reversed
  ) => Reverse original reversed


test1 :: SProxy "EDCBA"
test1 = SProxy :: forall output. Reverse "ABCDE" output => SProxy output

test2 :: SProxy "ABCDE"
test2 = SProxy :: forall output. Reverse "EDCBA" output => SProxy output

test3 :: SProxy "NEKO!"
test3 = SProxy :: forall output. Reverse "!OKEN" output => SProxy output

ConsではなくAppendを使っているところがありますが、これは結合するときに先頭のSymbolが1文字であるとは限らないからです(Consでは先頭のSymbolは1文字でなければなりません)。

この例では、各テスト関数の型定義を_(ワイルドカード)にしても、エラーにならず、導出結果の逆順のSymbolを教えてくれます。

1
1
0

Register as a new user and use Qiita more conveniently

  1. You get articles that match your needs
  2. You can efficiently read back useful information
  3. You can use dark theme
What you can do with signing up
Sign upLogin
1
1