Pre-Scheme
NewsProjectsReferencesRoadmapPre-Scheme is a statically typed dialect of the Scheme programming language, combining the flexibility of Scheme with the efficiency and low-level machine access of C. The compiler uses type inference, partial evaluation, and other correctness-preserving transformations to compile a subset of Scheme into C with no additional runtime overhead. This makes Pre-Scheme a vi
The Hackett Programming Language
WARNING: The contents of this manual are considered unstable, experimental, and subject to change; compatibility will not be maintained. Hackett is a statically typed, pure, lazy, functional programming language in the Racket language ecosystem. Despite significant differences from #lang racket, Hackett shares its S-expression syntax and powerful, hygienic macro system. Unlike Typed Racket, Hacket
Introduction - Typechecker Zoo
Press ← or → to navigate between chapters Press S or / to search in the book Press ? to show this help Press Esc to hide this help Typechecker Zoo This is a pet project of mine I’ve been working on for a while. We’re going to create minimal implementations of the most successful static type systems of the last 50 years. This will involve making toy implementations of programming languages and the
Loogle!
About Loogle searches Lean and Mathlib definitions and theorems. You can use Loogle from within the Lean4 VSCode language extension using (by default) Ctrl-K Ctrl-S. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot. Usage Loogle finds definitions and lemmas in various ways: By constant: 🔍 Real.sin
Rustで単一化を書くスマートな方法を考えた
課題 Rustでシンプルな単一化を書くことを考えます。単一化は主に型推論の実装に用いられます。 ここでは以下の方針で実装します。 一階の単一化。 変数は非負整数のidで表現し、0から順に付番する。 変数以外の項はRustのADTを使った通常の木構造で表現し、ノードの共有は行わない。 変数参照の縮約は行わない。 この方針のもと実装すると、およそ以下のようなコードになります。 #[derive(Debug, Clone)] pub struct UnifyEnv { vars: Vec<Option<Type>>, } #[derive(Debug)] pub struct UnificationFailure; #[derive(Debug, Clone, PartialEq, Eq)] pub enum Type { Var(usize), Constr { constr: u32, ar
いろんなプログラミング言語のアドホック多相 - Qiita
TL;DR アドホック多相は型クラスじゃなくても実現できる。 Haskell, Rust, Scalaでは後付けで拡張できるけど、それはアドホック多相の本質ではない。 アドホック多相(Ad hoc polymorphism) ウィキペディアは辞書ではないのはわかっていますが、それでも 英語版WikipediaのAd hoc polymorphismのページを参考に挙げておきます。 ざっくりまとめると 型階層上は関連性のない複数の型の引数に適用できる、多相的な関数 引数の型に応じて、個別の（アドホックな）実装にディスパッチされる と、それだけのこと。 「引数の型によって別の実装にディスパッチされるって、それメソッドのオーバーロードと何が違うの」ってことなんですけど、特に違いはありません。同じです。とはいえ、プログラミング言語によって、実現方法や使い勝手は違います。そのあたりのことを、いくつか
あなたのPythonを100倍高速にする技術 / Codon入門
はじめに Pythonは世界的にも人気のあるプログラミング言語ですが、実行速度については課題があります。Pythonの実行速度を高速化したい、という要求は根強く、これまでにも様々なツールや処理系が開発されています。 この記事ではMITの研究者らが開発したPythonを高速化するツール「Codon」について紹介します。 この記事を3行でまとめると： 高性能で簡単に扱えるPythonコンパイラ「Codon」 Pythonとの互換性がありながら、CやC++に匹敵する高速化を実現 実際にPythonコードが100倍速くなることを検証 Codonとは Codonは高性能なPythonコンパイラです。実行時のオーバーヘッドなしにPythonコードをネイティブなマシンコードにコンパイルし、シングルスレッドで10-100倍以上の高速化が実現できます。Codonの開発はGithub上で行われており、2021
BLisp: A Statically Typed Lisp Like Language
BLisp is a statically typed Lisp like programming language which adopts effect system for no_std environments. BLisp supports higher order RPC like higher order functions of functional programming languages.
Zig 言語用ライブラリ basis-concept を書きました - ::Eldesh a b = LEFT a | RIGHT b
Zig 言語用のライブラリ basis-concept を書きましたのでその紹介をします。 > github.com/eldesh/basis_concept 序 Zig は手続き的な型付き言語です。表現力としては、型上のコンパイル時計算によりアドホック多相を表現出来ます。 ただし型コンストラクタや部分特殊化が無いため、型の分類をシステマチックに行うのが面倒になっています。 このライブラリは型上の述語によって基本的な型の分類方法とそれらの上のジェネリックな関数を提供するユーティリティーライブラリです。 Concept このライブラリでは型を分類するための述語をコンセプトと呼びます。主なコンセプトを紹介します。 Eq 等値比較を可能な型です。== で比較でき、かつポインタを含まない型は自動的にこのコンセプトを満たします。eq と ne という関数を持っている型の場合もこのコンセプトを満たしま
Zig の文書読んで所感を記す - Qiita
これは何？ Zig を学ぼうと 公式文書 (0.91時点) を読んでいるんだけど、読みながら思ったことを記していく。 続編は Zig の文書読んで所感を記す #2 へ。 その前に Zig への言及が最近多いなぁ、でもシンプルな言語だって言うしまあどうでもいいかなぁ、ぐらいの気持ちでいたんだけど、ZigはCMakeの代替となるか を読んで、俄然興味が湧いてきて、じゃあ読んでみるか、と思った。 数値 i32 とか u16 のような名前で型が提供されている。 整数は 128bit まである。そればかりか、 3bit とか 53bit のような中途半端な幅の整数も使える模様。面白い。 さらに。何に使うのかわかってないけど、 i0 u0 のようなゼロビットの整数もある。 ちなみに0ビット整数には 0 が代入できる。 u1 は、 0 または 1。 i1 は、 0 または -1 が代入可能。 浮動小数点
Goにおける型によってSQLインジェクションを防ぐ方法
はじめに 2022年のセキュリティ・キャンプ全国大会に講師として参加しました。その際に、Goにおける脆弱性への対策はどうなっているのか調べました。この記事では、github.com/google/go-safeweb/safesqlがどのようにSQLインジェクションを防いでるのかについて解説します。 なお、@rungさんの文書を多いに参考にしております。また、セキュリティ・キャンプで用いた資料はこちらから閲覧できます。 SQLインジェクションとは？ 独立行政法人情報処理推進機構（IPA）が公開している安全なウェブサイトの作り方を見ると、SQLインジェクションは以下のように説明されています。 データベースと連携したウェブアプリケーションの多くは、利用者からの入力情報を基にSQL文（データベースへの命令文）を組み立てています。ここで、SQL文の組み立て方法に問題がある場合、攻撃によってデータベ
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
GitHub - coalton-lang/coalton: Coalton is an efficient, statically typed functional programming language that supercharges Common Lisp.
Moogle: Semantic search over mathlib4
String と &str｜Rust の文字列の種類と変換トレイトについて
GitHub - google/zerocopy: Zerocopy makes zero-cost memory manipulation effortless. We write `unsafe` so you don’t have to.
GitHub - hsk/tapl
GitHub - rudynicolop/TAPL-Coq: Coq implementations of and proofs of properties of typed-languages in Benjamin Pierce's Types and Programming Languages
GitHub - lucadp19/TaPL-Haskell: Languages from "Types and Programming Languages" implemented in Haskell.
https://www.researchgate.net/publication/228985001_Typing_Functional_Stack-Based_Languages
stal.dvi