A minimalistic example of bidirectional type checking for system F
Main.hs Sf�XU �� �XU {-# LANGUAGE StrictData, DerivingVia, OverloadedRecordDot #-} {- (compiled with GHC 9.4.2) -} {- HEADS UP this is an example implementation of a non-trivial type system using bidirectional type checking. it is... - naive: a real implementation would use more advanced techniques such as NbE, elaboration to core, debruijn representation, and various optimizations - minimal: ther
それ、モノイド(Monoid)でできるよ
この Scrap について TODO 全てのサンプルコードには以下の import が存在している前提でお読みください。
多相関数を第一級で取り扱う
今回は，GHC拡張の一つ RankNTypes の紹介をしようと思う．もうちょっとちゃんとまとめたのをいつか Haskell-jp かどっかに投稿したいと思ってるんだが，時間が (さっさと書け)． さて， Haskell のプログラミングにおいて多相関数はかなり重要な役割を持つ．しかしながら，標準の範囲では多相関数自体を第一級の値として扱うことはできない．私たちに許されるのは，多相関数を定義することだけだ．まあ，それだけでもかなり有用なんだけど，多相関数を第一級で扱えると，色々プログラミングの幅が広がる．今回は，多相関数を第一級として扱うというのはどういうことか，そしてそれをするにはどうすればいいか，そうすることで何がうれしいのかを簡単に触れられたらと思っている． 多相関数を第一級で扱うとはどういうことか (パラメトリック)多相関数 ((parametric) polymorphic fu
Rustのトレイトは「高カインド多相のない型クラス」である - なんか考えてることとか
Rustのトレイト（以降Rustトレイトとつなげて呼ぶことにする）は一体何なのか、様々な他言語の概念を通して調べていたが、やっと（「やはり」でもあるのだが）結論が出たので書いていこうと思う。 また、Rustトレイトはインターフェースなのか、MixInなのか、はたまたトレイトなのかということについて書き直したかったのでそれもついでに書く。 Rustのトレイトにおける否定 前置き Rustのトレイトはインターフェースではない RustのトレイトはJavaのインターフェースではない RustのトレイトはC#のインターフェースではない RustのトレイトはMixInではない Rustのトレイトはトレイトではない Rustのトレイトは「高カインド多相のない型クラス」だった 根拠1: 型クラスと用法が同じである 根拠2: 重複する関数があった際の挙動も同じ Rustのトレイトでは高カインド多相ができな
Type Sets Proposal 勉強会 (2021/08/01 13:00〜)
概要 GoのType Sets Proposalについて勉強する会です。 事前にNobishiiさんの資料 (下記) を読んだ上で、気になる箇所について議論します。 Go の "Type Sets" proposal を読む - Zenn Type Sets Proposalを読む(2) - Zenn また、事前にType Parameters Proposalに目を通しておくことをおすすめします。 オンライン (Google Meet) で行います。 進め方 Nobishiiさんの資料を上から読みつつ、気になった部分についてフリートーク形式で議論します。 議論中にType Sets Proposal本体も参照します。 参加者がType Setsについての理解を深めることを目的にするので、事前に資料を読んでおく必要はありますが、必ずしも深く理解している必要はありません。 議論したいポイント
パターンマッチの網羅性検査
解決策１：パターンマッチをコンパイルするとき、「すべてのパターンが失敗したらexit 1する」コードをパターンマッチの最後に追加する。 解決策２：コンパイル時にパターンの網羅性を検査する。 解決策２のほうが望ましそうなので、解決策２を目指す。そのためには、パターンの網羅性を検査する処理を実装しなければならない。そのための情報収集を行う。
Higher Kinded Types - herp-technote
例えばHKTの無いOCamlでは､'a list は型ではなく型コンストラクタという扱いになっているが､HKTのあるHaskell(List A または [A])では * → * という A型を受け取って[A]を返す型である｡ 式を取って式を返すという関数が式であるとさまざまな実りがある(c.f. ラムダ計算)ように､型を受け取って型を返すという仕組みも型に含まれているとさまざまな嬉しさがある｡
Go の "Type Sets" proposal を読む
Intro 読者の想定知識 この記事で出てくるGo言語仕様用語 サマリー Context Type Parameters Proposalの要点 Type listの必要性 暗黙的な"underlying type matching"の問題 type listからsum typeへ underlying type matchingと代入可能性 underlying type matchingと型switchステイトメント underlying type matchingの表現力の限界 Type Sets Proposal Type sets(型集合) 型Tがinterface ITを実装するための条件 要素を埋め込んだインタフェースのtype set interface elements(インタフェース要素) 任意の型(インタフェース型に限らない) approximation elemen
Another Generic Dilemma
Another Generic Dilemma Feb 24, 2021 In “The Generic Dilemma”, Russ Cox observes that you can have only two of separate compilation unboxed values parametric polymorphism (but see 1 and 2 for how you can achieve a middle ground with enough compiler wizardry) Now that Go is getting generics, I want to point out another dilemma: Any language has parametric polymorphism, eventually If you start with
RustのHigher-Kinded type Trait | κeenのHappy Hacκing Blog
κeenです。少し前の話になりますがRustの関連型を駆使してHigher Kinded type Trait（高階型トレイト）を実現してしまったものが出回ってたのでそれについて。 本来RustはHKTをサポートしていませんが不思議なことに実装出来てしまっているのです。 HKTについて微塵も知らない方にも分かるように解説していきます。 map 可能なトレイト Option、Result、etc 色々なトレイトが map メソッドを実装しています。 それぞれ型シグネチャを抜き出してみましょう。 Option: map<U, F: FnOnce(T) -> U>(self, f: F) -> Option<U> Result: map<U, F: FnOnce(T) -> U>(self, op: F) -> Result<U, E> 驚く程似てますね。これを抽象化して「mapメソッドを持つ」
Javaによる型制約を持ったインスタンスメソッドの模倣 - ロジニキ雑記
概要 Javaではレシーバーが特定のParameterized Typeである時のみ呼び出す事が出来るインスタンスメソッドを定義するという言語機能はありません。しかし、Parameterized Typeを引数に取る関数を外部で定義し、ジェネリック型には外部から渡された関数を自身のインスタンスで評価するメソッドを定義する事により模倣することができます。 型制約 インスタンスメソッドを呼び出す事が出来る条件として型変数の継承関係を取る事を本記事では型制約と呼びます。 型制約のモチベーションを確認するために次のコードを考えましょう。 public final class Holder<T> { private final T t; public Holder(T t) { this.t = t; } public T t() { return t; } // ネストしたHolderを「潰す」
kadai1
課題４ 線形型に関する論文を読んでそれに基づく型推論プログラムを書く 線形型システムとは？ 線形型システムとは、プログラム実行中に作られた値が何度使われうるかによって 型を区別するような型システムです。例えば、整数の型はMLの型システムでは単に"int" ですが、 線形型システムでは、高々一回しか使われない整数の型は"int<１>", 何回でも使われうる 整数の型は"int<ω>" のように区別されます。このように型の概念を拡張しても MLと全く同じように自動的に型推論が行なえる （ここでは型の概念が拡張されていますから、 各データが何回使われるかも自動的に推論されることになります）ことが最近になって知られており、 例えば、fn x=>x+1 の型は、∀ｉ>=1, ｊ.(int<ｉ> -> int<ｊ>) のように推論できます。 線形型って何の役に立つの？ プログラム実行中に高々一度しか使
【Kotlin】try-catch がやりにくければ runCatching を使ってみよう！ - Qiita
例外がスローされたらあれを実行したいが、 スローされなかったらこれを実行したい。 そういうときありますよね。 try-catch（-finally）では書きにくいときがある try-catch（-finally）では、 例外がスローされたときの処理（とスローされてもされなくてもする処理）は書けても、 スローされなかったときの処理は単純には書けません。 例で考えてみましょう。 まず、例外がスローされることを考えなくてよい場合を考えます。 fun noException() { val myValue = getMyValue() // 値を取得する。 .also { onMySuccess(it) // その後 onMySuccess を呼び出す。 onMyFinally() // 最後に onMyFinally を呼び出す。 } setMyValue(myValue) } ここで getM
Arrowの紹介その１
Picapp アドベントカレンダー初日です。 唐突にはじまりましたが、普段みんなが気になっている技術だったり仕事で利用しているものだったり、エモい話を書きたい人が書くアドベントカレンダー（のはず）です。 とりあえず言い出しっぺの私が初日と二日目を埋めますので、どうぞよろしくおねがいします。 Λrrow（以下Arrow）というLibraryをご存知でしょうか? Λrrow is a library for Typed Functional Programming in Kotlin. とあるように、関数型プログラミングのためのライブラリです。 というとなんだか怖いイメージが生まれてしまそうですが、 今回はこのArrowの中のDataTypesから幾つかとっつきやすそうなものを紹介していこうと思います。 なお基本姿勢ですが… 基本的に公式Documentと動画、KotlinSlackの#arr
F-ing Modules, yabaitech.tokyo vol.5
yabaitech.tokyo vol.5にはgfn(@bd_gfngfn)さんによる「F-ing modules の型検査とコンパイル手法」という記事があり、それを読んだので、気になった箇所について書いたり、ついでにF-ing Modulesに関する補足などをしていきます。 F-ing Modulesとは初めに、F-ing Modules自体について説明しておきます。F-ing modulesとは、Rossberg, Russo, Dreyerの3人による、次の2つの論文を指します。 F-ing Modules (TLDI, 2010)F-ing Modules (JFP, 2014)著者によるプロジェクトサイトもあります。Russoの博士論文とDreyerの博士論文は、MLのモジュールシステムの論文の中でも特に有名な論文で、その2人が関わっているだけあってよく書かれています。 MLのモ
Rust の `!` (ビックリマーク、エクスクラメーションマーク、感嘆符、never) 型 - Don't Repeat Yourself
タイトルは記号のググラビリティ確保のためにわざとつけています（笑）。動作はすべて、Rust 1.47.0 (stable) です。nightly を使用した場合は nightly と文中に記載しました。 TL; DR Rust には ! という「何も返さないことを示すモノ」が存在する。 never 型と呼ぶ。 値を何も返さない計算の表現として使用される。 普段は型強制される（ので、使っていることに気づかないかも）。 never 型は安定化されていない。 TL; DR 基本 ! = never 型 never 型はどこに出てくるのか Coercing 発展 never 型はまだ安定化されていない std::convert::Infallible で、なんで Rust には ! がいるの？ Rust ではなぜ、関数の戻り値だけにしか ! を使用できなくしてあるの？ 今回も記事が長くなってしまい
Background: how we got the generics we have (Or, how I learned to stop worrying and love erasure)
原文はこちら。 This article was written by Brian Goetz (Java Architect, Oracle). http://cr.openjdk.java.net/~briangoetz/valhalla/erasure.html ジェネリクスの方向性を語る前に、まず、ジェネリクスの現在の状況とそこまでの経緯を語る必要があります。この文書では、現在のジェネリクスが、いま作ろうとしている「より良い」ジェネリクスへどのように影響を与えるかの礎として、主として現在のジェネリクスがどのようにしてできあがったのか、そしてその理由についてフォーカスします。 特に、2004年にJavaにジェネリクスを追加する際には、実際にはerasure（消去、ここではtype erasure、つまり型消去を意図している）が賢明で実用的な選択であったこと、そして、erasureによ
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
Applicative勉強会
Swiftで高カインド多相
ScalaのOptionクラスのソースコードを読んでみた | メンバーズエッジカンパニーブログ