執筆中：「Haskellでの型レベルプログラミング」 | 雑記帳
最近、「Haskellでの型レベルプログラミング」という「本」を執筆している。まだ完成ではないが、以下のリンクから読める： Haskellでの型レベルプログラミング なぜHaskellか 最近いろんな言語が出てきている中で、Haskellの強みとは何だろうか。人によって答えは色々あるだろうが、筆者にとってHaskellの魅力的な側面は強力な型システムである。どのくらい強力かというと、型レベルでプログラミングができ、依存型の模倣さえもできてしまう。 （依存型をやりたいなら最初から依存型のある言語を使えという意見は尤もだが、それはそれとして。） Haskellでの型レベルプログラミングの解説記事というのは、英語圏ではちらほら見かけるが、日本語圏ではあまり見ない。2018年（原文は2017年）に公開された Haskellにおける型レベルプログラミングの基本(翻訳) – Qiita が数少ない例で
型安全で高速な連鎖行列積の計算
この記事は Haskell Advent Calendar 2021 の22日目の記事です。 次のような３つの行列の積を考えてみましょう。 ABC = \begin{pmatrix} a_{00} & a_{01} & a_{02} \\ a_{10} & a_{11} & a_{12} \\ a_{20} & a_{21} & a_{22} \\ a_{30} & a_{31} & a_{32} \\ \end{pmatrix} \begin{pmatrix} b_{00} & b_{01} \\ b_{10} & b_{11} \\ b_{20} & b_{21} \\ \end{pmatrix} \begin{pmatrix} c_{00} & c_{01} & c_{02} & c_{03} & c_{04} \\ c_{10} & c_{11} & c_{12} & c_{13}
Haskellの型パズルで作るMini Interpreter
「効率よく素数を計算するプログラムを作る課題」を出したら「コンパイル時に素数判定を行うプログラムが優勝した」なんて話がありますが[要出典]、今回は型レベル文字列で数式を渡すとコンパイル時に計算を行ってくれる型レベルインタプリタを作ってみようと思います[1] 動作イメージはこんな感じ > :kind! Calc "(1 + 1) * (2 + 0) + 10" Calc "(1 + 1) * (2 + 0) + 10" :: Nat = 14 GHCiで :kind! を使うと与えられた型の型シノニムや型族による変換を評価してくれます。つまり上記のプログラムは数式を表す型レベル文字列を評価してNatカインドの14という型に評価されているというわけです。 元ネタはQuramyさんのこの記事です 今朝この記事を引用した友人が 「文字列型を型レベルで扱える似たような機能って他の静的型付け言語にもあ
Five benefits to using StandaloneKindSignatures - Ryan Scott
GHC 8.10.1 is slated to be released soon, and among the improvements that it offers is the new StandaloneKindSignatures language extension. Standalone kind signatures (or “SAKS” for short) are like type signatures, except that they describe type-level declarations instead of term-level values. Here is one example of a standalone kind signature that describes the kind of a type synonym: {-# LANGUAG
テンソル形状のコンパイル時検査＋実行時アサーション化を今のHaskellで書いてみる - Qiita
はじめに Edward Z. Yang 氏の記事 A compile-time debugger that helps you write tensor shape checks は、テンソルの形状の検査を依存型でコンパイル時に対話的にやりつつ、静的に決まらない部分や静的な検証が難しい部分はアサーションとして実行時検査に遅延するという仕組みの提案。 対話的なアサーションの挿入部分とかはともかく、型付けとアサーションの部分は今のHaskellでも大体出来るなぁと思ったので試しに書いてみた。 (元記事自体Haskellっぽい構文で書かれているし、 Edward Z. Yang 氏自身、ここまでは出来るのは当然知って書いているのだと思うけれど) 結果 元記事での、アサーションを挿入した最終的なプログラムは以下:
jaspervdj - Dependent Types in Haskell: Binomial Heaps 101
Who put binary numbers in my type system? Published on September 4, 2018 under the tag haskell Haskell eXchange Update: I gave a talk about this blogpost at the Haskell eXchange 2018 on the 11th of October 2018. You can watch the video here. Note that you will need to create an account in on the skillsmatter website in order to watch the recording. Introduction This post makes a bit of a departure
Lysxia - Haskell with only one type family
In this post, we will implement open type families with a single actual type family.1 Surprisingly, this endeavor leads to increased expressivity: type families become first-class. Check out my very creatively named package: first-class-families. The result is a form of defunctionalization (I call “eval-style”), to be compared later with a more common one (“apply-style”). I will not assume knowled
Type-Directed Code Generation :: Reasonably Polymorphic
Update 2019-05-30: Formation finally got around to opensourcing the work done here. https://github.com/formationai/proto-lens-grpc aka “Type-Level Icing Sugar” Context🔗 At work recently I’ve been working on a library to get idiomatic gRPC support in our Haskell project. I’m quite proud of how it’s come out, and thought it’d make a good topic for a blog post. The approach demonstrates several type
しりとりの圏の回答、または定理証明Haskellを少しだけ - Qiita
この記事は、Haskell (その2) Advent Calendar 2017 の4日目の記事です。 同アドベントカレンダーの5日目の記事、しりとりの圏の実装(未完) の問題を解いてみたのと、その際に定理証明Haskellのちょうどいい例題が出て来たので、解説してみます。 なお4日目の記事が5日目の記事のアンサーになるのは時空間の歪みによるもので正常な動作です。日付順に読まれている方については、申し訳ございませんが5日目の記事に飛んでいただけるようお願い致します。 idを定義するために さしあたって、しりとりの圏を構成するSiriの定義を、親記事より拝借します。 {-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE TypeApplications #-
しりとりの圏の実装(未完) - Qiita
haskell入門 の著者の一人、hirataraです。といっても、このエントリは書籍とはまったく関連のないお遊びです ということで、今回は10年ほど前のエントリである しりとりの圏 を、Haskellで実装しようと試みましたので、その過程をだらだらと書いていきます。 前置き しりとりの圏とは以下のようなものです。 対象(Object)は文字 'あ' 'い' 'う' ・・・ 射(Morphism)は文字列 "はすける" :: 'は' -> 'る' 恒等射(Identity)は一文字 "あ" : 'あ' -> 'あ' 合成は文字列の結合 "るびー" . "はすける" == "はすけるびー" この圏は直感的にわかりやすい圏で、圏論の初学者が集合圏以外の圏に触れるきっかけとしてはちょうどよい題材と言えます。 しかし、「圏論と言えばHaskellだろう」と安易に考えてこの圏をHaskellのプログ
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
Haskellでの型レベルプログラミング
Compile Time Type Level C Compiler (this may indicate out of memory)
Type Witnesses in Haskell
GitHub - kcsongor/regex-type: Regular expression matching of Haskell types
GitHub - isovector/type-sets: type level sets
GitHub - sheyll/type-spec: A tiny EDSL to write type-level-unit tests
GitHub - mstksg/lens-typelevel: Type-level lenses using singletons because why not
GitHub - mstksg/decidable: Combinators for manipulating dependently-typed predicates.
tyfam-witnesses
Introduction to Singletons (Part 1)
