Generalized Algebraic Data Types in ATS
Bluish Coder Programming Languages, Martials Arts and Computers. The Weblog of Chris Double. The ATS programming language supports defining Generalized Algebraic Data Types (GADTS). They allow defining datatypes where the constructors for the datatype are explicitly defined by the programmer. This has a number of uses and I'll go through some examples in this post. GADTs are sometimes referred to
Binary instances for GADTs (or: RTTI in Haskell)
In this blog post we consider the problem of defining Binary instances for GADTs such as If you want to play along the full source code for the examples in this blog post can be found on github. Failed attempt The “obvious” way in which you might attempt to serialize and deserialize Val could look something like instance Binary (Val a) where put (VI i) = putWord8 0 >> put i put (VD d) = putWord8 1
GADTs Meet Their Match: Pattern-Matching Warnings That Account for GADTs, Guards, and Laziness
GADTs Meet Their Match: Pattern-Matching Warnings That Account for GADTs, Guards, and Laziness Georgios Karachalias Ghent University, Belgium georgios.karachalias@ugent.be Tom Schrijvers KU Leuven, Belgium tom.schrijvers@cs.kuleuven.be Dimitrios Vytiniotis Simon Peyton Jones Microsoft Research Cambridge, UK {dimitris,simonpj}@microsoft.com Abstract For ML and Haskell, accurate warnings when a func
GADTを用いた型安全なCPS変換の実装 - autotaker's blog
概要 CPS変換とはラムダ項と継続を入力として型Xを持つラムダ項を出力するプログラム変換である。 HaskellのGADTという機能を使うと型Tを持つラムダ項を表すデータ型Term Tを定義できる。 CPS変換が正しいことは cps :: Term T -> Term ([T] -> X) -> Term Xという型がつくことで表現される。 （ここで[T]は型TをCPS変換した型） GADTは表現力の高いDSLであるが、parse :: String -> Maybe (Term T)のような関数を書くことはできないため、標準入力からラムダ項を受け取りcps関数に渡すためには少し工夫がいる。 今回はtypeCheck :: Term' -> A -> (forall T. Term T -> A) -> A という関数を実装することでこの問題を解決した。 実装は以下で公開されている。git
Why GADTs matter for performance
When GADTs (Generalized Algebraic Data Types) landed in OCaml, I wasn’t particularly happy about it. I assumed that it was the kind of nonsense you get when you let compiler writers design your programming language. Which is to say that the standard GADT examples all seem to be about the kinds of things that compiler writers do, like embed domain-specific languages or build typed abstract-syntax t
Detecting use-cases for GADTs in OCaml
I’ve been interested in GADTs1 for quite some time now but I’ve had a hard time finding proper use-cases for them in my day-to-day programming tasks; this is not because GADTs aren’t useful, they are, but rather that my understanding of them has been limited. I often experience this when I’m learning more advanced features of programming languages and I’ve found that I personally find it easier to
Wadler's Blog: ADT and GADT implementations of simply-typed lambda calculus
Lennart Augustsson posted a nifty description of a compiler from a simple expression language to LLVM that included a conversion from expressions represented as an ADT to expressions represented as a GADT. The ADT requires a separately implemented type checker, while the GADT piggybacks on Haskell's type system to ensure expressions are well typed. However, Lennart's expression language does not i
New draft on Normalization by Evaluation using GADTs
There is a new draft on my web page! It is called Tagless and Typeful Normalization by Evaluation using Generalized Algebraic Data Types, which is a mouthful, but only describes accurately the cool new OCaml development we elaborated together with Olivier and Chantal. The world of Normalization by Evaluation (NbE) is still relatively new to me, but its wonders keep amazing me. It’s a program speci
GADTによるHaskellの型付きDSLの構築 - プログラミングの実験場
GADTについて、この解説が分かりやすい（英語）。 http://en.wikibooks.org/wiki/Haskell/GADT 背景 Haskell（というか関数型言語一般）の素晴らしい機能の一つ、代数的データ型を使うと、抽象構文木(AST)をHaskellの枠組みの中で表現できる。 例えば、整数の足し算・引き算ならば、 data Exp = Const Int | Add Exp Exp | Subtract Exp Exp さらにこのASTを数値一般に使いたいので型パラメータrをつけて多相にしてみる。 data Exp r = Const r | Add (Exp r) (Exp r) | Subtract (Exp r) (Exp r) これを使えば、例えば(3 + 4) - 2という数式は、Subtract (Add (Const 3) (Const 4)) (Const
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
Domain Driven Design using GADTs
GitHub - reflex-frp/reflex-gadt-api: Interact with a JSON-serialized API defined by a GADT in your reflex-dom application
Sketch.sh - Interactive ReasonML/OCaml sketchbook
Stitch: The Sound Type-Indexed Type Checker
https://tech.bezoomnyville.com/2015/12/07/A-GADT-implementation-of-AVL-tree.html
http://www.math.nagoya-u.ac.jp/~garrigue/papers/gadtspm.pdf
Photo Tourism: Microsoft Research, Interactive Visual Media Group
Reddit - Dive into anything
OCaml-TLS: ASN.1 and notation embedding | MirageOS
Representing pattern-matching with GADTs
http://www.cs.unibo.it/~puech/typeful.pdf