タグ検索の該当結果が少ないため、タイトル検索結果を表示しています。
これは筆者（κeen）がIdris Advent Calendar 2020に投稿した内容を土台とし、一冊の本になるように増補改訂を行なったものです。 本書では依存型のあるHaskellことIdrisについて紹介します。Idrisは純粋関数型言語であり構文もHaskellに似ていますが、大きな特徴として依存型があることが挙げられます。依存型があるとリストの長さを指定したり整数同士の割り算でゼロ除算が起きないことを保証したり、究極的には数学の証明をしたりもできます。また、依存型以外にもインタラクティブな開発環境を使った型駆動開発であったりElaborator Reflactionによるメタプログラミングだったりと注目に値する言語機能も揃っています。 総じてIdrisは非常に尖った言語です。作者がプログラミング言語理論の研究者ということもあり、かなり攻めた言語機能が入っています。依存型を搭載し
# Idris2の数量的型が解決した問題導入した問題 ---------------------- [第一回関数型プログラミング（仮）の会 - connpass](https://opt.connpass.com/event/222709/) === # About Me ---------  * κeen * [@blackenedgold](https://twitter.com/blackenedgold) * GitHub: [KeenS](https://github.com/KeenS) * GitLab: [blackenedgold](https://gitlab.com/blackenedgold) * [Idein Inc.](https://idein.jp/)のエンジニア * Lisp, ML
Idrisでふんわり眺める依存型
どうも，よわよわエンジニアです．前回の記事では，TAPLを読んで型システムに入門しました． その記事の中で，1つ腑に落ちなかったことがあります．そう， 依存型 です． 依存型は，TAPLでも発展的内容として深く触れないんだっピ… よわよわエンジニアがTAPL（型システム入門）を読んだら 依存型は，関数型，全称型，型演算子に続いてラムダキューブを完成させる最後のピースでした． それが埋まらず，日々ストレスを貯める一方だったのですが，はてブのコメントで「実戦で色々試したくなったらIdrisがあるよ!!」と親切な方が教えてくださったので， 依存型の雰囲気を味わうためにIdrisへふんわり入門してみます． 依存型ってなんやねん 型にプログラムが書けるってどういうこと プログラミングと証明に何の関係があるんだ といった疑問を解決するまでの日記です． Idrisとは Idris=Haskell+依存型
import Data.String data FizzBuzz = F | B | FB | I Integer Show FizzBuzz where show F = "fizz" show B = "buzz" show FB = "fizzbuzz" show (I n) = show n fizzBuzz : Integer -> FizzBuzz fizzBuzz n = case (n `mod` 3, n `mod` 5) of (0, 0) => FB (_, 0) => B (0, _) => F _ => I n fizzBuzzSeq : Integer -> List FizzBuzz fizzBuzzSeq n = map fizzBuzz [1..n] main : IO () main = do [_, arg] <- getArgs | _ => put
このエントリはIdris Advent Calendar 2020の19日目の記事です。 次はmock_beginnerさんでIdrisとはじめる型駆動開発です。 κeenです。今回はこのAdvent Calendarの山場の1つ、定理証明について解説しようと思います。 依存型で証明ができる原理 カリー＝ハワード同型対応といって、プログラムのと論理学の定理には対応関係があることが知られています。 これはすなわち、我々が普段プログラムを書いているときは同時に論理学の命題を証明していることでもある、ということです。 そんな大それたことしてないよーと思うかもしれませんが、それもそのはず。 普通のプログラムではあまり面白い命題を表現できないので、わざわざ証明というほどでもないからです。 しかしIdrisには依存型があります。 依存型があると型の表現力が上がるので対応する論理学の命題の表現力が上がり
The Qiita Advent Calendar 2020 is supported by the following companies, organizations, and services.
Why is Idris 2 so much faster than Idris 1? - Edwin Brady
I've just released a new version of Idris 2, which is a significant release in that it's the first one which is able to compile itself. Thus, it's the first one where we can really see how the performance of Idris 2 improves on the performance of Idris 1. A question people sometimes ask when discussing Idris on various parts of the Internet is "Why is Idris 2 so much faster than Idris 1?" Sometime
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
プログラング言語Idrisに入門させたい（v0.9）
Idris 2の数量的型が解決した問題、導入した問題 | κeenのHappy Hacκing Blog
依存型のあるHaskellことIdrisってどんな言語？ | κeenのHappy Hacκing Blog
Idrisで依存型を使った定理証明入門 | κeenのHappy Hacκing Blog
Idrisのカレンダー | Advent Calendar 2020 - Qiita
news.yahoo.co.jp
obaken-event.wixsite.com
news.yahoo.co.jp
news.yahoo.co.jp
news.yahoo.co.jp
news.yahoo.co.jp