pkm.watasuke.net

Idris

3 min read

純粋関数型 プログラミング言語

A purely functional programming language with first class types

  • Idris 1とIdris 2があって、後者はまだ正式リリースされていない（v1.0.0未満）らしい
    • 開発が止まっている？
      • 2025-05-04時点での最終リリース日は、前者 (1.3.3) は2020-05-24で後者 (0.7.0) は2023-12-22
      • メーリングリスト (Google Group)もほぼ止まっている
        • 最新の投稿は2025-03-28（カンファレンスの勧誘？）だがその前は2024-09-24
      • Idrisの開発を始めた人？については、GitHubの草は生えていないがMastodonでは活動しているらしい
  • Idris 1についてのわかりやすい記事（Zennの本）がある：プログラング言語Idrisに入門させたい（v0.9）
  • Idris 2について、
    • 公式ドキュメントっぽいのはこれ：Documentation for the Idris 2 Language — Idris2 0.0 documentation
    • 起動時に読み込まれるpreludeのAPIと標準ライブラリ的なbaseのAPI
      • preludeには四則演算を行う関数（演算子？）とかIOとかBoolとかListとかがある
      • baseにはEitherとかMaybeとかFileとかがある
        • Idris 1のbase にはData.Complexがあったらしいけど2にはないね
      • docs.rsのほうが便利だな
        • 検索機能とかないんですかね
    • ライブラリの実装はGitHubのlibs/下にある
      • たとえば libs/prelude/Prelude/Basics.idr を見ると、関数結合演算子が如何様に定義されているのかを知ることが出来る 
        (.) : (b -> c) -> (a -> b) -> a -> c
(.) f g = \x => f (g x)
    • idris2 で REPL を起動できる
      • :s で検索ができる
      • びっくりするほど便利 
        Main> :s List Char -> String
Prelude.pack : List Char -> String
   Turns a list of characters into a string.
   Totality: total
   Visibility: public export
Prelude.fastPack : List Char -> String
    • idris2 <filename> -x main で mainを実行できる

Graph View