AIに依存型をサポートした言語ai-langを作ってもらった件

表題の通りです。最近話題のClaude Codeに「一から依存型サポートした言語作ってよ」（に相当する英語）で一行命令出しただけで、あとはClaude Codeがほぼ自律的にコーディング。ツール利用許可出した以外は手出しせずに5000行近くのコードが生産されたのですから凄いものです。

できた言語はこちら

• 多相的なデータ型が定義できない（多相関数はあり）
• 暗黙の引数が使えない（ので、全部明示的に渡す必要がある）

といった制限はあるものの、以下のようなプログラムが動きます。さすがに依存型＋多相型になるとClaudeも苦戦したようで、その辺りの実装はかなり進みが遅くなっていたのが印象的でした。構文の見た目は特に指定しなかったのですが、Agda2辺りから拝借してきたのでしょうか。

ともあれ、現状のAIに対してポン出しでここまで行けるのはやはり感動的ですね……5時間待つのはつかれましたが。

-- Basic ai-lang example

-- Natural numbers
data Nat : Type where
  Z : Nat
  S : Nat -> Nat

-- Booleans
data Bool : Type where
  True : Bool
  False : Bool

-- Basic arithmetic
add : Nat -> Nat -> Nat
add Z y = y
add (S x) y = S (add x y)

sub : Nat -> Nat -> Nat
sub Z _ = Z
sub x Z = x
sub (S x) (S y) = sub x y

-- Boolean operations
not : Bool -> Bool
not True = False
not False = True

-- Comparison
isZero : Nat -> Bool
isZero Z = True
isZero (S _) = False

-- Identity function (polymorphic)
id : {A : Type} -> A -> A
id x = x

-- Constant function (polymorphic)
const : {A : Type} -> {B : Type} -> A -> B -> A
const x _ = x

-- Example values
two : Nat
two = S (S Z)

three : Nat  
three = S two

five : Nat
five = add two three

-- Main result
main : Nat
main = five