Idris

https://gyazo.com/3822ca006166090b85b3dc9dc0fbe3a2

バックエンドもいろいろ

C, LLVM, Java, JavaScript

型クラス的なやつ

入門記事

2013年のもの

repl

$ idris

:load hoge.idr

ファイル読み込み

:watch hoge.idr

監視読み込み

:exec main

main関数を実行

ライブラリのimportは？

:t

型の確認

:quit

終了

compile

$ idris hoge.idr -o hoge

そして、遅い

run

$ ./hoge

型クラスやdo構文もあるが、遅延評価ではない

Haskell実装コンパイラでCにコンパイルして、gccなどでコンパイル

IO

Haskellとだいたいおなじ

インタプリタで実行すると変な感じになる

code:idr

greet : IO ()

greet = do putStr "What is your name? "

name <- getLine

putStrLn ("Hello " ++ name)

mutualブロック

Idrisでは宣言の順番によって使える関数が変わる

自分より下に書いた関数は使えない

mutualブロックを書けばそれを回避できる

Haskellはdefaultでできる

IO

だいたいHSと同じ

遅延評価

ネタ

参考

2011?

作者が書いた？

あどかれ