Lean4によるプログラミングを行うにあたって、自分用にまとめたメモになります。
基本的にHaskellライクな文法ですが、定義にdefを利用したり、:=(束縛)と=(等号)を区別するなど、細部で違いがあるので、Haskellと差異がある点を中心に簡単にまとめていきます。
※ 実行環境の構築は少々古いですがこちらにまとめたものがありますので、参照してください。
定義
関数や変数の定義にはdef, letを利用します。
defはグローバル定義、letはローカル定義用になります。
def global_var := 10
def method : String :=
let word := "Hello,"
word ++ " World"
また、Haskellとは異なり、letで複数の変数を一度に定義できません。
-- 以下の様には記述できない
let x := 10
y := 20
-- 必ず1つずつ定義する必要あり
let x := 10
let y := 20
-- どうしても定義したい場合はタプルを利用すると可能
let (x, y) := (10, 20)
代入 (束縛)と等号
変数の代入(束縛)には:=を利用します。
def x := 10
def method : String :=
let word := "Hello"
word ++ ", World"
=は代入ではなく等価判定となります。
IO.println (10 == 10) -- true
関数の型定義
引数は(a : Nat)の様に定義します。
引数が複数存在し同一型である場合は、(a b : Nat) の様に省略して記述できます。
以下の2つの定義は等価です。
def add1 (a : Nat) (b : Nat) : Nat := a + b
def add2 (a b : Nat) : Nat := a + b
ラムダ式に関しても同様です。
def add3 := fun (a : Nat) (b : Nat) => a + b
def add4 := fun (a b : Nat) => a + b
文字列補間 (String Interpolation)
pythonのフォーマット文字列のような機能がlean4にもあります。
以下の様に利用します。
def withHello(s : String) : String :=
s!"Hello, {s}!"
#eval withHello "World" -- Hello, World!
簡易的な値のチェック
#evalを利用すると、現在の状態を簡易的にチェックすることができます。
ただし、IOなどの副作用を伴うような操作はチェックできません。
VSCodeのLean 4拡張機能をインストールしておき、以下の様に記述すると、InfoView上に30と表示されます。
#eval 10 + 20
以下の様に副作用を伴う操作の場合、エラーになります。
#eval IO.getStdin
ただし、副作用があっても疑似ランダム生成の様なケースの場合は評価可能です。
以下の評価を行うと毎回値が異なります。
#eval IO.rand 1 100
配列とリスト
リストや配列的な構造としては以下の様なものがあります。
- List
- Array
- Vector
リストは以下の様に記述します。
単純に[]で記述すれば配列になります。自動推論できるような単純な定義の場合、型定義を書かなくてもコンパイルが通ります。
def ls1 : List Int := [1, 2, 3, 4]
def ls2 := [1, 2, 3, 4]
配列は以下の様に記述します。
リスト表記の先頭に#を記述すると配列になります。こちらも自動推論ができる場合、型定義は明示的に記述しなくてもコンパイルが通ります。
def as1 : Array Int := #[1, 2, 3, 4]
def as2 := #[1, 2, 3, 4]
ベクトルは以下の様に記述します。
リスト表記の先頭に#vを付与するとベクトルになります。
依存型であるので、要素数の記述も必要です。
こちらも自動推論ができる場合、明示的な型定義は不要です。
def vs1 : Vector Int 4 := #v[1, 2, 3, 4]
def vs2 := #v[1, 2, 3, 4]
ラムダ式と高階関数
ラムダ式で利用する変数は、式が簡易的である場合は、以下の様に省略して記述できます。
-- 省略せずに記述したもの
List.foldl (fun x y => x + y) 0 [1, 2, 3, 4] -- 10
-- 変数を省略したもの。変数を"."で表す
List.foldl (. + .) 0 [1, 2, 3, 4] -- 10
mapやfoldlなどの高階関数は、Listなどの配列系のデータ構造側に定義されているので、以下の様に.を利用してより簡易的に記述できます。
[1, 2, 3, 4].foldl (. + .)
クラスの拡張
既存のクラスを拡張して独自のメソッドを追加することができます。
リストの要素数を求める処理としてList.lengthがありますが、同様の処理を自前で実装すると以下の様になります。
def len {a : Type} (xs : List a) : Nat :=
match xs with
| [] => 0
| _ :: rest => 1 + len rest
この定義の場合、以下の様に利用することになりますが、Lean4の場合、クラス自体を拡張することができます。
IO.println len [1, 2, 3, 4] -- 4
以下の様に.を利用して、追加したい関数を記述できます。
リスト型に直接追加しているので、.を利用してそのまま呼び出すことができます。
-- "."による関数追加
def List.len {a : Type} (xs : List a) : Nat :=
match xs with
| [] => 0
| _ :: rest => 1 + len rest
-- 利用例
IO.println $ [1, 2, 3, 4].len -- 4
Option型
Lean4では、MaybeではなくOptionを利用します。
HaskellではJust/Nothingを利用していましたが、Lean4ではsome/noneを利用します。
let x : Option Nat := some 10
match x with
| some v => IO.println s!"x is {v}" -- ← ★ こっちが出力される
| none => IO.println "x is none"
let y : Option Nat := none
match y with
| some v => IO.println s!"y is {v}"
| none => IO.println "y is none" -- ← ★ こっちが出力される
マクロ
Lean4にはマクロ機能があります。
以下の様に直感的に利用しやすい形式になっています。
macro マクロ名 引数 : 戻り値の型 => `(式)
引数の2倍にするマクロ twice は以下の様に記述できます。
-- twiceマクロの定義
macro "twice" x:term : term => `($x + $x)
-- 呼び出し
IO.println $ twice 20
戻り値がMonadの場合は以下の様に記述できます。
-- doブロックを利用しているので戻りはMonadになる
macro "twiceM" x:term : term => `(do
let a := $x
pure $ a + a
)
-- 呼び出し
IO.println =<< twiceM 20
引数を2つ以上定義する場合は、以下の様に中間に何かしらの文字列を挟む必要があります。
引数が3つ以上のケースでは、2つ定義することになりますが、同一にする必要はありません。
-- 引数2、引数3のパターン
macro "madd2" x:term " and " y:term : term => `($x + $y)
macro "madd3" x:term " and " y:term "&" z:term : term => `($x + $y + $z)
-- 呼び出し
IO.println $ madd2 10 and 20
IO.println $ madd3 10 and 20 & 30
また、引数の両側にも何かしらの文字列を指定することができるので、以下の様に数学でおなじみの絶対値記号を実装することもできます。
-- 絶対値マクロ
macro "|" x:term "|" : term => `(Int.natAbs $x)
-- 呼び出し
IO.println $ |-3| -- 3
その他の詳細に関しては以下のドキュメントを参照してください。