型の理論 入門概要プレスルーム著作権お問い合わせクリエイター向け広告掲載開発者向け利用規約プライバシーポリシーとセキュリティYouTube の仕組み新機能を試してみる© 2024 Google LLC
型の理論入門 （ 論理学入門 III ） | MaruLabo
型の理論入門 概要 「型の理論」には、Russellの 'Ramified Type Theory' から Voevodsky の 'Homotopy Type Theory' までを数えれば、100年以上の歴史があります。 「型の理論」の歴史には、ひとつ大きな特徴があります。 ラッセルの理論が、自ら発見した「集合論の逆理」がもたらした数学の基礎の「危機」を解消しようとする試みとして生まれたことが示すように、「型の理論」は数学をどのように基礎づけるかという問題と結びついて発展してきました。 Churchのラムダ計算もTuringのTuring machineの構成も、ゲーデルの不完全性定理がもたらした数学の基礎についての「危機」に対する反省・探究の中で生まれたものです。数学の基礎への関心は、集合論、Topos理論にかわる数学の新しい基礎づけを目指したVeovodskyの"Univalent
モナドの使い方 - Haskell 入門
モナドの使い方 Maybe モナド Haskell では Maybe 型をよく使う。Maybe 型の data 宣言は次のようになる。 Prelude> :info Maybe data Maybe a = Nothing | Just a -- Defined in `Data.Maybe' Maybe 型のデータコンストラクタは Nothing と Just a だ。検索が失敗したときは Nothing を返し、検索が成功したときはその値を Just "foo" のようにして返すというような使い方をする。Prelude には標準の関数でペアのリストからキーの値が fst 要素に一致するペアの snd 要素の値を求める lookup という関数がある。この lookup の戻値が Maybe 型だ。 Prelude> lookup 3 [(1,'a'),(2,'b'),(3,'c')]
代数的データ型 - ウォークスルー Haskell
代数的データ型（algebraic data type）とは，図のように木構造で表現される値からなるデータ型のことです． 配列のような一部の例外を別とすれば，Haskell で取り扱うあらゆるデータ型は代数的データ型です．
Haskell のセクションと中置記法
1. セクションの特徴は何？ Haskell の2項演算子に対して部分適用したものをセクションと呼ぶ。 ふつうのHaskellプログラミング によると、 部分適用を使い引数を1つだけ渡した二項演算子のことを特にセクション (section) と言い、普通の部分適用とは少し違った特殊な機能が用意されています。 (p205) 「部分適用とは少し違った特殊な機能」とはなんだろう？ 部分適用については、以下を参照。 cf. Haskell における関数の型と、部分適用 セクションとは、Haskell 98 Report: 式 によると、 セクション は ( op e ) あるいは ( e op ) のように書く。ここで、op は 二項演算子であり、e は式である。セクションは二項演算子の部分適 用をあらわすのに便利な構文である。 2. 二項演算子を関数として用いる 二項演算子とは、演算子 - Wi
Haskell 16日目 〜 関数合成と部分適用 〜 - 理想未来ってなんやねん
Haskell 16日目。 関数合成 関数合成(function composition)とは、複数の関数を合成して新しい関数を作ることです。 例えば、文字列に含まれる行数を数える関数、numberOfLinesは$演算子を使って記述すると次のように書けます。 numberOfLines :: String -> Int numberOfLines cs = length $ lines cs 上記の関数は関数合成を使うと次のようにも書けます。 numberOfLines :: String -> Int numberOfLines = length . lines (.)関数は、２つの関数を合成する関数です。 『合成する』とは、『2つの関数を順番に適用する新しい関数を作る』ということで、例えば(length . lines)は、『引数にlines関数を適用し、その値にlength関数を適
capm-network.com - このウェブサイトは販売用です！ - capm network リソースおよび情報
This webpage was generated by the domain owner using Sedo Domain Parking. Disclaimer: Sedo maintains no relationship with third party advertisers. Reference to any specific service or trade mark is not controlled by Sedo nor does it constitute or imply its association, endorsement or recommendation.
関数型プログラミングなんもわからん。を考えようと言うイベントを開きました。
先日Connpassにて、関数型プログラミングなんもわからん。を考えようと言うイベントを開かせていただきました。 関数型プログラミングがわからない！ と言う方達の疑問に対して、普段関数型プログラミング言語を使っているわかる人たちが回答をして行くと言うスタイルのイベントでした。関数型プログラミング言語と一口に行っても、Elm, Scala, Haskell, Clojure, Elixir, F#と様々な言語があり(これは今回参加した人たちの使っている言語で、関数型プログラミング言語の一部にしか過ぎません)何が正解かなどはわからない中での意見の集約といった形のため参考程度にご覧ください。結果イベントとしては様々な視点からの意見が聞けて満足という声が多かったです。私自身知らないことがたくさん知れて勉強になり楽しかったです。 イベントの内容は、Figma上で開けるFigJamファイルとして、公開
チャーチ＝チューリングのテーゼ - Wikipedia
チャーチ＝チューリングのテーゼ (英: Church-Turing thesis) もしくはチャーチのテーゼ (英: Church's thesis) とは、「計算できる関数」という直観的な概念を、帰納的関数と呼ばれる数論的関数のクラスと同一視しようという主張である。テーゼの代わりに提唱（ていしょう）あるいは定立（ていりつ）の語が用いられることもある。このクラスはチューリングマシンで実行できるプログラムのクラス、ラムダ記法で定義できる関数のクラスとも一致する。よって簡単にはテーゼは、計算が可能な関数とは、その計算を実行できるような有限のアルゴリズムが存在するような関数、よっておおよそコンピュータで実行できる関数と同じだと主張する。 概要[編集] 1932年にエルブラン、および1934年にゲーデルが、原始帰納的関数と呼ばれる自然数上の関数の明示的構成法を拡張して帰納的関数（もしくは一般帰納的
Functors, Applicatives, And Monads In Pictures - adit.io
Written April 17, 2013 updated: May 20, 2013 Here's a simple value: And we know how to apply a function to this value: Simple enough. Lets extend this by saying that any value can be in a context. For now you can think of a context as a box that you can put a value in: Now when you apply a function to this value, you'll get different results depending on the context. This is the idea that Functors
HaskellのLinearTypes言語拡張について少し調べた - TSUGULOG
最近リリースされた GHC 9.0.1 で使えるようになった LinearTypes 言語拡張について気になったので調べた。 LinearTypes言語拡張とは GHC9.0.1から使えるようになった言語拡張で、Linear Typeを導入できる。ただ、上記リリースノートに “a first cut” とある通り、まだ実験的な機能としてリリースされた段階のようだ。 通常のGHCの言語拡張のように とすることで使えるようになる Linear Typeとは そもそもLinear Typeとはどのような概念なのか、簡単に説明すると、「関数の引数がちょうど1度だけ評価される」、という条件を指定できるもののようだ。 理論的な基礎となるLinear type systemsについては前から広く知られていたものの、なかなか実装までは至らず、今回Haskellで晴れて実装までこぎつけたとのことだった。 具
Haskell に IDE はないのか？──独断と偏見による Haskell の IDE 十年史
答え：Haskell に IDE はずっとある、今ならHLS使え（内容を読む気がないようという人向けの答え） はじめに 2021年2月現在、Haskell の IDE 環境は Haskell Language Server (HLS) の登場により劇的な進化を遂げていますが、日本の Haskell コミュニティではその前身の Haskell IDE Engine (HIE) の情報がまだ氾濫しており、十分な周知に至っていない現状があります。 本稿では、こうした現状を打破すべく、2021 年 2 月現在の Haskell の IDE 環境を取り巻く現状と、そこに至るまでの歴史を完全に独断と偏見で紹介します。より多くの人に HLS の存在を周知し、皆さんの Haskell Life の一助となれば幸いです。また、HLS の前身である HIE は必ずしも快適に動作するとは言い難かったため、HLS
矢印のパターンで理解する Functor〜Applicative〜Monad - Qiita
F[A]→F[B] に至る矢印を比べて、いろいろな型クラスをまとめて理解する、Cats 入門者向け記事。 はじめに この記事では、Cats の型クラスをテーマにする。 Cats は関数型な Scala プログラミング1のためのライブラリなので、この記事でも関数を扱う。関数型パラダイムで関数2というと数学の関数とだいたい同じだから、定義域の集合から値域の集合へのマッピングのことになる。ただし、数学では写像や射などと言うが、記号でも矢印（→）だし、図の上でも矢印なので、この記事では矢印ということにする。 また扱う型クラスとしては、Functor、Applicative、Monad の周辺をメインとする。前半ではそれらの Scala トレイトが要求する実装必須メソッドのうち、F[A]→F[B] に向かう矢印に還元できるもの3に着目して整理し、さらに後半では、それらの周辺に見られるもう一つのパター
カリー＝ハワード同型対応 - Wikipedia
関数型プログラムとして書かれた証明：自然数の加法に関する交換律のCoqによる証明。 カリー＝ハワード同型対応（カリー＝ハワードどうけいたいおう、英語: Curry–Howard correspondence）とは、プログラミング言語理論と証明論において、計算機プログラムと証明との間の直接的な対応関係のことである。「プログラム＝証明」(proofs-as-programs)・「型＝命題」(formulae-as-types)などとしても知られる。これはアメリカの数学者ハスケル・カリーと論理学者ウィリアム・アルヴィン・ハワード（英語版）により最初に発見された形式論理の体系とある種の計算の体系との構文論的なアナロジーを一般化した概念である。通常はこの論理と計算の関連性はカリーとハワードに帰属される。しかしながら、このアイデアはブラウワー、ハイティング、コルモゴロフらが定式化した直観主義論理の操作
Terminal Coalgebra as Directed Limit
Terminal Coalgebra as Directed Limit Posted by Bartosz Milewski under Programming 1 Comment Previously, we talked about the construction of initial algebras. The dual construction is that of terminal coalgebras. Just like an algebra can be used to fold a recursive data structure into a single value, a coalgebra can do the reverse: it lets us build a recursive data structure from a single seed. Her
iOSDC Japan 2018 で発表した「圏論とSwiftへの応用」の補足
この記事は、 iOSDC Japan 2018 で圏論について話しました ＋ Storyboard/AutoLayout相談会しました - Qiita の続編です。 先週、8月30日〜9月2日にかけて開催された iOSDC Japan 2018 で登壇発表した 「圏論とSwiftへの応用」 の補足になります。 CfP / スライド CfP: 圏論とSwiftへの応用 by 稲見 泰宏 | プロポーザル | iOSDC Japan 2018 - fortee.jp Slide: 圏論とSwiftへの応用 / iOSDC Japan 2018 - Speaker Deck スライドメモ： iOSDC Japan 2018 「圏論とSwiftへの応用」発表スライドメモ - Qiita まとめ: 圏論とSwiftへの応用 @inamiy #iosdc #c - Togetter 動画: https
Scala3と圏論とプログラミング - Qiita
最近、圏論とプログラミングという素晴らしい資料を拝読しました。圏論とプログラミング愛に溢れる資料で読んでいて目頭が熱くなりました。そうだよな・・・プログラマにも圏論いるよな・・・ ただ、自分にとって残念だったのは、資料で説明用に選択されたプログラミング言語が「Haskell」だったことです。もちろんHaskellは素晴らしい言語です。ただ、自分にとってHaskellは外国語なのでちょっと理解が難しいのです。なのでこの資料が「Scala」で書かれていたらと夢想せずにはいられなかったのです。 Scalaと言えば昨年末にScala3のリサーチコンパイラのDottyがFeature Completeを宣言しました1。この宣言で新機能の追加は終了して、あとは2020年末のリリースに向けてひたすら品質を上げていく段階に突入しました。つまり、ようやく次世代のScalaが全貌を現したということです。 ここ
iOSDC Japan 2018 「圏論とSwiftへの応用」発表スライドメモ - Qiita
この記事は、先日の iOSDC Japan 2018 で発表した 「圏論とSwiftへの応用」 のスライドメモです。 来月10月16日に開催される プログラマのための圏論勉強会 - connpass の予習用の入門資料としてお使いください。 （さらに勉強したい方は、 圏論のオススメ勉強法（プログラマ向け） を合わせて読むと、キャッチアップしやすいと思います） スライド・動画・補足記事 Slide: 圏論とSwiftへの応用 / iOSDC Japan 2018 - Speaker Deck 動画: https://www.youtube.com/watch?v=zvrgfsDfxf8 関連記事: 圏論のオススメ勉強法（プログラマ向け） iOSDC Japan 2018 で発表した「圏論とSwiftへの応用」の補足 - Qiita それでは発表を始めます。 本日のテーマは 「圏論」 です。
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
A Gentle Introduction to Haskell: Patterns
遅延評価 - OCaml.jp