プログラミング言語処理系が好きな人のミートアップ第78回

お久しぶりです。Malgoを作ってるtakoeight0821（星にゃーん）です

前回参加したのが2023年。あれから色々ありました…

zikuの話

腱鞘炎が悪化して、結構コーディングが厳しくなりました

AIコーディングに全Betしてます

100%AI製のプログラミング言語&プログラミング言語処理系

プログラミング言語と処理系の設計は人間

関連技術の調査とコーディングはAI

code:example.ziku

-- zipWith: combines two codata streams element-wise

let rec zipWith = {

# f s1 s2 .head => f s1.head s2.head,

# f s1 s2 .tail => zipWith f s1.tail s2.tail

} in

-- take: convert first n elements of a stream to a Cons/Nil list

let rec take = \n => \s =>

if n == 0 then Nil

else Cons(s.head, take (n - 1) s.tail)

-- fib: Fibonacci stream with three explicit copattern cases

let rec fib = {

#.tail.tail => zipWith { # x y => x + y } fib fib.tail

} in

-- First 5 Fibonacci numbers as a cons list

take 5 fib

Expected result: Cons(0, Cons(1, Cons(1, Cons(2, Cons(3, Nil)))))

採用技術

実装言語はLean 4

Schemeにコンパイル

Copattern matching and Codata

AgdaとかにあるCopattern matchingをサポート

その値が「どう使われるか」でパターンマッチできる記法

期待するメソッドチェーンのパターンと、対応する振る舞いを記述する

コンパイルアルゴリズムは大学時代の研究成果を使ってる…はず

IR based on Sequent Calculus

シークエント計算ベースの中間表現を採用

式を「値を生み出す式 Producer」と「値を消費する式 Consumer」に分ける

ProducerとConsumerを取って何らかの計算を行う文がいくつかある

気持ち扱いやすいCPSみたいな感じ

詳しくは『Grokking the Sequent Calculus』を読んでくれ！