ソート

代数において、ソート (sort) はプログラミング言語の型 (type) に対応する概念である。CafeOBJ は強く型付けされた言語である。

ソートは [ ... ] を使って宣言する:

[ <sort-name> ... <sort-name> ]

<sort-name> にはソート名を記述する。ソート名をスペースで区切って、複数のソートを一度に宣言することができる。ソート名は、Nat のように頭文字を大文字で記述することが多い (慣習) 。

ソート宣言の例:

[ Node Edge ]

この例では、2つのソート Node と Edge を宣言している。

ソート間の包含関係

CafeOBJ では、包含関係を持つソートを宣言することができる。例えば、自然数と整数を表すソート Nat と Int がある。CafeOBJ では、Nat は Int に含まれる、と宣言することができる。あるソートに含まれるソートをサブソート (subsort) 、あるソートを含むソートをスーパーソート (supersort) と呼ぶ。先程の例では、Nat は Int のサブソートであり、Int は Nat のスーパーソートである。なお、ソート間の包含関係は循環してはならない。

ソート間の包含関係を宣言するときは、ソート宣言中に < で表現する。

[ <subsort-name> < <supersort-name> ]

ソート宣言の例:

[ NzInt < Int ]

2つのソート NzInt と Int を (直感的には、0 でない整数と、0 を含む整数) 宣言している。サブソートは部分関数を宣言する際に良く用いられる。例えば、整数上の積 (*) と除 (/) を宣言するとき、積は全関数であるが、除は部分関数であることを次のように定義できる:

  op _*_ : Int Int -> Int
  op _/_ : Int NzInt -> Int

このように宣言すると / の第二引数に 0 が与えられた演算は未定義となる。

[Next] 輸入

Original Copyright © Takahiro Seino, all rights reserved.