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
Rewriting the Coreutils in ATS
I wanted to give a small demonstration of ATS, partly to document a little bit of how to use atspkg, partly to show how to (safely) beat C's performance in ATS, and partly an example of how to parse command-line arguments in ATS. We won't do a full implementation of wc here, but hopefully this post will give an indication of how one would do such a thing. Installing ToolingIf you are on Linux or M
Session Types in a Linearly Typed Multi-Threaded Lambda-Calculus
We present a formalization of session types in a multi-threaded lambda-calculus (MTLC) equipped with a linear type system, establishing for the MTLC both type preservation and global progress. The latter (global progress) implies that the evaluation of a well-typed program in the MTLC can never reach a deadlock. As this formulated MTLC can be readily embedded into ATS, a full-fledged language with
ATS2の依存型を使ってAVL木 | κeenのHappy Hacκing Blog
κeenです。少しばかりATS2を触ってみたので成果報告でも。 AVL木は左右のノードの高さが高々1しか違わない平衡二分木です。OCamlやSMLでナイーブに実装すると本当に1しか違わないことを保証するのは難しく、精々テストなどで部分的に検査するだけです。 ところがSMLに似た文法を持つATS2には依存型があり、左右のノードの高さが高々1しか違わないことを型で保証出来ます。 つまり、左右のノードの高さが2以上違う木を作ろうとしてもコンパイルエラーになるのでコンパイルが通れば高さについてはバグがないこと保証されます。 そういうAVL木を使ってTreeSetを作ってみたので紹介します。 私のブログ(のこの記事)の読者ならATS2も依存型もAVL木も知ってそうですが一応説明します。 ATS2って何? 詳しい説明は日本ATSユーザグループに譲るとして、この記事にて重要な点を挙げます。 SMLに似た
Specific Endpoints
Email Submitted successfully Thank you for subscribing to our newsletter! It’s not the daily increase but daily decrease. Hack away at the unessential. —Bruce Lee As a web application developer, many of the x-unit style tests that I write assert simple relationships among data. When applications begin to grow, the constraints imposed by these relationships are sometimes strengthened through additi
likai @ cs-people - ML programmer's guide to ATS
In this guide, we don't aim to teach you programming in ATS (Applied Type System), but we need to tell you enough so that a seasoned ML programmer can quickly adjust to the terminology used in ATS and start reading existing ATS code. In ATS, it is useful to keep in mind that you will be programming in three worlds. Dynamics, the part that evaluates when you run the program. This is what programmer
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
ATS: Why Linear Types are the Future of Systems Programming
Writing basic proofs in ATS
Practical ATS
"A (Not So Gentle) Introduction To Systems Programming In ATS" by Aditya Siram
matzにも解るよう、禅問答的に #ATS2 の型理論を説明してみたよ