こわくない Idris (6) - M59のブログ こわくない Idris (6) - M59のブログ 1年前に書いた記事を読み返していたら、証明がすぐには理解できなかった。証明の内容を言葉で分かるように書いておきたいと思う。次のコードのMyHead.headは、全域函数だ。 %default total namespace MyHead head : (l : List a) -> (isCons l = True) -> a head Nil prf = FalseEli…

IdrisからJavaScriptのAPIを叩いてみる。 module Main getElementById : String -> IO Ptr getElementById s = mkForeign (FFun "document.getElementById(%0)" [FString] FPtr) s setInnerHTML : String -> Ptr -> IO String setInnerHTML s e = mkForeign (FFun "%1.i…

Idrisみたいに、函数プログラミングを前提にしている言語には函数を合成する演算が標準で用意されているよね。 (.) : (b -> c) -> (a -> b) -> a -> cこの演算子を使うと、函数を合成してくれる。函数の合成を使えば、プログラムを変数を使わないで書くことができる。 整数を文字列にする : Integer -> String 整数を文字列にする = show 最初の文字を得る : String -> Char 最初の文字を得る = strHead 整数…

…納 制限された再帰 Idrisには函数が全域函数であるかチェックする機能があるのだけれども、プログラムに制限なく再帰が使われていると、その函数が値を返すのか、それとも停止しないで値が返らないままなのか判定する方法が存在し得ない。そこで、Idrisでは再帰呼び出しの引数の値が「減少」する場合にはその函数は停止する、そうでない場合には停止しないかもしれない、というように判定する。 再帰呼び出しの引数が「減少」するというのは、要はその函数が帰納的に定義されているということだ。引数が…

…headとは異なり、IdrisのPrelude.List.headは、引数にコンスセルである証明をとるので、全域函数になっている。Idrisのシステムでは次のように、%assert_total宣言によって、全域函数であることが「表明」されている。 %assert_total head : (l : List a) -> (isCons l = True) -> a head (x::xs) p = xここでは、自分でhead函数が全域函数であることを「証明」をしてみよう。 %…

…なっている。例えば、Idrisにおける、Listに対するhead函数は次のような型を持っている。 head : (l : List a) -> (isCons l = True) -> aこれは、第1引数にリストを取る他に、第2引数にそのリストがコンスセルである（Nilでない）「証明」を要求していることになる。もし isCons l = True が証明できなければ、そのような型を持つ値を渡すことができず、型が合わないから型検査時にエラーになる。 Idris> head [1…

…ひとつ返ってくる。 Idrisでは、函数が全域函数であるかどうかを調べることができる。 foo : a -> Maybe a foo x = Just x bar : Maybe a -> a bar (Just x) = x baz : Bool -> () baz False = () baz True = baz True函数 foo, bar, baz はどれも型チェックが通る。しかし、 bar と baz は全域函数ではない。 idris total.idr を実行…

…たとえばこうなる。 Idris> the (Exists Nat (\n => Vect n Integer)) (Ex_intro 4 [1, 2, 3, 4]) (4 ** [1,2,3,4]) : (n ** Vect n Integer)\n => Vect n Integer というのは、単なるラムダ記法である。型の表現に普通の函数を用いることができることが分かる。この部分は flip Vect Integer と表現することもできる。REPLの出力は奇妙な表示にな…

…rやListの宣言はidrisではこうなっている。 data Either a b = Left a | Right b data List a = Nil | (::) a (List a)このようなデータ型宣言を行うと、型コンストラクターと値コンストラクターが定義される。Idrisでは型も値だから、型コンストラクターも値コンストラクターも同様に函数として扱われ、大文字小文字関係なく使うことができる。型コンストラクターは型を返す函数であり、値コンストラクターはその型の値を返…

はじめに Idrisという、Haskellに似ていて、依存型 dependent type を持っている言語がある。依存型を持った言語なんて他にもあるのだけれども、Idrisは general purpose を謳っている。わざわざ汎用って謳っているあたり、依存型ってのはもっと色々に使えるものなんだぞって主張があるように思う。そんなIdrisなんだけど、日本語による文献はとても少ない。今のところ、Idrisをやろうって人はまず英語のチュートリアル読まなきゃいけない。僕はIdr…

…=> bind (\x' => Pure (f' x')) x) f instance Functor f => Monad (Free f) where return = Pure m >>= k = bind k m$ idris --check --total free.idr free.idr:8:Free.bind is possibly not total due to recursive path Free.bind --> Free.bindうまくいかないなー

…実行してみる。 $ idris -o stream stream.idr --total --warnpartial stream.idr:8:Warning - Main.iterate.0.#iterate' is possibly not total due to recursive path Main.iterate.0.#iterate' --> Main.iterate.0.#iterate' $ ./stream [O, sO, ssO, sssO, ssssO…

Idris http://idris-lang.org/ は依存型を持つ純粋関数型言語。C言語経由でネイティブコードを生成する他、JavaScriptコードの生成もできるようだ。*1cabalを使ってインストールする。 cabal update; cabal install idrisハローワールドのソースコード。IdrisはHaskell風の文法を持っている。型注釈は必要。 module Main main : IO () main = putStrLn "Hello wo…