Idris
依存型をもつ汎用言語
Haskellに似たシンタックス
Lazy型を使えば遅延評価できる ref
バックエンドもいろいろ
C, LLVM, Java, JavaScript
型クラス的なやつ
入門記事
@mandel59氏のブログシリーズ
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とだいたいおなじ
インタプリタで実行すると変な感じになる
idrgreet : IO ()
greet = do putStr "What is your name? "
name <- getLine
putStrLn ("Hello " ++ name)mutualブロック
Idrisでは宣言の順番によって使える関数が変わる
自分より下に書いた関数は使えない
mutualブロックを書けばそれを回避できる
なんでdefaultでしてないんだろう
Haskellはdefaultでできる
コンパイルが遅くなるとかあるのかな #??
IO
だいたいHSと同じ
遅延評価
ネタ
参考
2011?
作者が書いた？
あどかれ