Idris
Idris
Idrisについて練習

Idrisを学んでマスターしてみませんか？

ExercismのIdrisトラックに参加すると、 58個の演習 コードの自動分析 と マンツーマンのメンタリング、 すべて100%無料で利用できます。

Idrisトラックに参加する 演習を見る

Idrisについて

module EvenOdd

data Even : Nat -> Type where
  EZ : Even Z
  ES : Even n -> Even (S (S n))

ee : Even n -> Even m -> Even (n + m)
ee EZ m     = m
ee (ES n) m = ES (ee n m)

Exercismには、Idrisの58個のプログラミング演習があります。 抵抗器カラーデュオから抵抗器カラートリオまで。

Exercismでは、楽しくやりがいのある演習を通して、コンセプトの理解を試しながらプログラミングを上達させられます。

抵抗器カラーデュオ

抵抗器カラーデュオ

抵抗器で使われるカラーコードを数値に変換します。

ローマ数字

ローマ数字

現代のアラビア数字をローマ数字に変換します。

抵抗器カラートリオ

抵抗器カラートリオ

抵抗器で使われるカラーコードを、人が読めるラベルに変換します。

ExercismのIdris演習をすべて見る

Idrisの主な機能

Idris

依存型

安全第一！　コンパイル時に、プログラムの正しさを強く保証します。

純粋関数型

ラムダ計算に着想を得て、スコープやループは関数を定義して呼び出すことで表現します。

型クラス

型をクラスに分類することで、型安全なオーバーロードが可能になります。

マルチスレッド

データが不変なので、より安全で考えやすい並行処理が可能になります。

コンパクト

Idrisが備えている汎用的な機能は、ごくわずかです。

革新的

Idrisは、活発に開発が進む研究用のテストベッドです

Idris流のメンタリングを受ける

プログラミング言語にはそれぞれ、物事の進め方があります。Idrisも 同じです。メンターが、Idrisのエンジニアのように 考える方法と、Idrisらしいコードの書き方を 教えてくれます。演習を解いたら、ボランティアチームに 提出してみましょう。ヒントやアイデア、フィードバックをもらい、 Idrisでよく目にする書き方に近づけることができます。 自分が知らないことを知らない、ということに気づかせてくれるでしょう。

メンタリングについてもっと詳しく

コミュニティが作ったIdrisの演習

ExercismのIdrisトラックには、58つの演習があり、より良いコードを書くのに役立ちます。

Idrisの演習をすべて見る
Idris

Idrisトラックを始めましょう

何より、誰にとっても100%無料です。

Idrisトラックに参加する