Idrisの人気記事 7件 - はてなブックマーク

1 - 7 件 / 7件

新着順人気順

絞り込み

検索対象
ブックマーク数
期間
セーフサーチ

Idrisの検索結果1 - 7 件 / 7件

タグ検索の該当結果が少ないため、タイトル検索結果を表示しています。

Idrisに関するエントリは7件あります。プログラミング、 books、 Haskell などが関連タグです。人気エントリには『プログラング言語Idrisに入門させたい（v0.9）』などがあります。

プログラング言語Idrisに入門させたい（v0.9）
- 19 users
- zenn.dev/blackenedgold
- テクノロジー
- 2021/05/01
これは筆者（κeen）がIdris Advent Calendar 2020に投稿した内容を土台とし、一冊の本になるように増補改訂を行なったものです。本書では依存型のあるHaskellことIdrisについて紹介します。Idrisは純粋関数型言語であり構文もHaskellに似ていますが、大きな特徴として依存型があることが挙げられます。依存型があるとリストの長さを指定したり整数同士の割り算でゼロ除算が起きないことを保証したり、究極的には数学の証明をしたりもできます。また、依存型以外にもインタラクティブな開発環境を使った型駆動開発であったりElaborator Reflactionによるメタプログラミングだったりと注目に値する言語機能も揃っています。総じてIdrisは非常に尖った言語です。作者がプログラミング言語理論の研究者ということもあり、かなり攻めた言語機能が入っています。依存型を搭載し
Idris 2の数量的型が解決した問題、導入した問題 | κeenのHappy Hacκing Blog
- 8 users
- keens.github.io
- テクノロジー
- 2021/10/01
# Idris2の数量的型が解決した問題導入した問題 ---------------------- [第一回関数型プログラミング（仮）の会 - connpass](https://opt.connpass.com/event/222709/) === # About Me --------- ![κeenのアイコン](/images/kappa2_vest.png) * κ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
- プログラミング
Idrisでふんわり眺める依存型
- 4 users
- sititou70.github.io
- 暮らし
- 2022/07/05
どうも，よわよわエンジニアです．前回の記事では，TAPLを読んで型システムに入門しました．その記事の中で，1つ腑に落ちなかったことがあります．そう，依存型です．依存型は，TAPLでも発展的内容として深く触れないんだっピ… よわよわエンジニアがTAPL（型システム入門）を読んだら依存型は，関数型，全称型，型演算子に続いてラムダキューブを完成させる最後のピースでした．それが埋まらず，日々ストレスを貯める一方だったのですが，はてブのコメントで「実戦で色々試したくなったらIdrisがあるよ!!」と親切な方が教えてくださったので，依存型の雰囲気を味わうためにIdrisへふんわり入門してみます．依存型ってなんやねん型にプログラムが書けるってどういうことプログラミングと証明に何の関係があるんだといった疑問を解決するまでの日記です． Idrisとは Idris=Haskell+依存型
依存型のあるHaskellことIdrisってどんな言語？ | κeenのHappy Hacκing Blog
- 4 users
- keens.github.io
- テクノロジー
- 2020/12/01
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で依存型を使った定理証明入門 | κeenのHappy Hacκing Blog
- 3 users
- keens.github.io
- テクノロジー
- 2020/12/23
このエントリはIdris Advent Calendar 2020の19日目の記事です。次はmock_beginnerさんでIdrisとはじめる型駆動開発です。 κeenです。今回はこのAdvent Calendarの山場の1つ、定理証明について解説しようと思います。依存型で証明ができる原理カリー＝ハワード同型対応といって、プログラムのと論理学の定理には対応関係があることが知られています。これはすなわち、我々が普段プログラムを書いているときは同時に論理学の命題を証明していることでもある、ということです。そんな大それたことしてないよーと思うかもしれませんが、それもそのはず。普通のプログラムではあまり面白い命題を表現できないので、わざわざ証明というほどでもないからです。しかしIdrisには依存型があります。依存型があると型の表現力が上がるので対応する論理学の命題の表現力が上がり
- あとで読む
Idrisのカレンダー | Advent Calendar 2020 - Qiita
- 3 users
- qiita.com/advent-calendar
- テクノロジー
- 2020/11/27
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
- 3 users
- www.type-driven.org.uk
- 暮らし
- 2020/05/26
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
- Idris

新着記事

キーボードショートカット一覧

j次のブックマーク

k前のブックマーク

lあとで読む

eコメント一覧を開く

oページを開く

設定を変更しましたx