type-level-programming

昔作ったやつのメモ。 Scala2でshapelessを使ってる。

以前書いた型レベル多項式をベースに型レベルに多項式の微分を実装する。 https://kazchimo.com/2021/05/19/dotty-typelevel-polynomial/ 多項式の定義とヘルパー型 以前の記事の再掲になるが...

scala3で登場したpolyfunctionを用いてscala2系で実現されていたpartially applied typeを改善する。 問題設定 例えばリテラル型を幽霊型として用いて、長さの情報を型レベルで保持するSizedListを...

\[mathjax\] dottyの柔軟な型を利用して型レベルの多項式とその一般の足し算を定義する。 多項式の定式化 まずはenumを用いて多項式の要素を型に落とし込む。 必要な要素は項とその足し算だ。 Xが項、Plusがその足し算を表して...

dottyの型システムに現れた強力な機能の一つにMatch Typeがある。 これによって2系のscalaだと信じられないくらい複雑なコードが必要だったものが簡潔になる。 Match Typeとは 受け取った型にパターンマッチをかけて指定の...

dottyでは型に対してコンパイル時に行える操作が色々増えている。 特にリテラル型に当たるものは値レベルの操作と遜色無いものが用意されている。 コンパイル時オペレーションの中でもscala.compiletime.ops以下に当たるパッケー...

scala3にはリテラル型がある。 実はだいぶ前からすでに存在していたのだが、そのサポートがより一層厚くなった。 リテラル型はTypeScriptによって広く一般に知れ渡り、その有用性が実証された。 例えばリテラル型を使用することでType...

shapelessとかを使って型レベルプログラミングしてるとAuxパターンを使ってメソッドの型シグネチャで計算を表現することになる。 しかしこれが結構曲者でscalaのコンパイラの残念さもあり結構大変である。 その際に起こるコンパイルエラー...

関数型やってるとよく聞く代数的データ型(ADT)について。 Scalaやってるとよく使うがHaskellほどこの話題について掘った記事はあんまりないのでdigっていきたい。 そもそも代数的データ型とは 具体例 こういうやつ。 なぜ代数的デー...

このドキュメントでordersky先生がscala3に入りそうなchecked exceptionのモチベを説明してくれていて、面白かったので紹介する。 該当のプルリク。 例外か否か 例外使うと正常系と異常系のパス別れてハッピーだよねみたい...

Scalaはなんとなく書けるようになったけどライブラリコードとか読めないし、関数型はもっとわかない。 特にF[]みたいなやついっぱい出てくるけどなに？みたいな人に捧げる記事です。 このようなものは高カインド型などと呼ばれ、なかなか理解が難し...