Idris

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

最新の投稿は2025-03-28（カンファレンスの勧誘？）だがその前は2024-09-24

Idrisの開発を始めた人？については、GitHubの草は生えていないがMastodonでは活動しているらしい

Idris 2について、

preludeには四則演算を行う関数（演算子？）とかIOとかBoolとかListとかがある

baseにはEitherとかMaybeとかFileとかがある

docs.rsのほうが便利だな

検索機能とかないんですかね

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

びっくりするほど便利