型推論と型検査、静的な型つけと動的な型つけ、強い型つけと弱い型つけ - sumiiのブログ
ついでに追加。 型推論：変数や式の型をプログラマが宣言しなくても、言語処理系が文脈から推論してくれる機構。MLとかHaskellとか。 型検査：変数や式の型が合っていることを言語処理系が（普通は静的に）チェックしてくれる機構。CとかJavaとか、MLやHaskellも。 静的な型つけ：プログラムの実行前に型を検査する機構。MLとかHaskellとかCとかJavaとか。 動的な型つけ：プログラムの実行中に型を検査する機構。LispとかSchemeとかPerlとか。 強い型つけ：検査を通れば、安全さ(safety)が保証される、という（普通は静的な）型つけ。MLとかHaskellとかJavaとか。Javaはバグがあったりしたので少し怪しいですが。 弱い型つけ：検査を通っても、安全さ(safety)は保証されない、という型つけ。CとかPascalとか。 安全さ(safety)：プログラムが言語仕
私と型システムとポエム
最近巷では俄に型システムについての言及が増え、型システムポエマーが増えてる気がするので自分もその時流に乗りたい。 完全にポエムだけどなんかあったら随時指摘ください。直します。 TL;DR 言いたいことはまとめると次 型システムは程度問題なのでちょうどいいところを探すべき 型は万能でも強さが正義でもない(だから未だに研究されてる) よく知りもしないくせに計算機科学を侮辱するのはやめろ 予防線 あくまでポエムですので中身はないです 私は型理論専攻で学位はとったものの研究者ではないのであまり信用しすぎないように 型システムの過去 型システムは大まかに次のような利点があるとされてきた(個人的主観) 「異常」なプログラムを検出する仕組み 静的解析による分かりやすいエラーメッセージ 型そのもののドキュメント性 IDEでのcompletionに貢献 最適化に貢献 (数学に正しく裏打ちされたsemanti
多相バリアントを使いこなそう(4) - osiire’s blog
前回までで多相バリアントの基本的な機能は説明してきました。そこで今回は、多相バリアントのとても重要な応用についてお話したいと思います。それは、場合分け構造の拡張問題です。 場合分け構造の拡張は難しい 例えば、次のようなコードがあったとします。 module Card = struct type t = Num of int | Jack | Queen | King let num = function Num i -> i | Jack -> 11 | Queen -> 12 | King -> 13 end Card.tには4種類の場合分けがあり、それらに対してnumという操作が定義されています。このような場合分け構造+操作に対して、 静的で安全に(キャストせず)、 元のコードを一切変更せず、 新しい場合分けを加え、 新しい操作も加えた 新しい場合分け構造を定義する にはどうすればいい
漸進的型付けの未来を考える - -
この記事はCAMPHOR- Advent Calendar 2017 11日目の記事です． アブストラクト 漸進的型付けは，ひとつの言語の中で静的型付けと動的型付けをスムーズに組み合わせるための技術です． よく知られた特徴は any 型を使った静的型付けで， TypeScript や Python といったプログラミング言語には既に実装されています． しかし，理論と実際のプログラミング言語の間には大きなギャップが存在します． 特に，漸進的型付けの理論で提案されているキャストを用いた動的型検査が実装されていないために， 静的型付けの恩恵を十分に得られていないという問題があります． この記事では，まず漸進的型付けの理論をコード例を用いて紹介し， 現状の漸進的型付き言語が抱える問題を解説します． そのあとで，漸進的型付き言語が目指すべき目標を理論的視点から論じます． それらの目標は，静的型付けを
Reddit - Dive into anything
I am reading Oleg Kiselyov's tutorial on tagless final interpreters. When implementing a DSL, what is the advantage of tagless final style over plain old datatypes (or say, GADTs)? I know when using normal datatypes, when you add new variants, you need to modify existing functions that operate on these types, and then you lose separate compilation. But does that really pose a huge problem in pract
tiger.dvi
Java 2 Standard Edition 5.0 Tiger Java 3 7 2013 10 25 Copyright 2004, 2005, 2009, 2010, 2013 Yoshiki Shibata. All rights reserved. iii Tiger, Tiger burning bright Like a geek who works all night What new-fangled bit or byte Could ease the hacker’s weary plight? – Joshua Bloch Tiger Java 2 Standard Edition 5.0 Java Java 1.1 1.4 assert 5.0 Java 5.0 1.4 Java 5.0 Java 1.4 1.4 5.0 5.0 5.0 Java type par
The DOT Calculus - (Dependent Object Types)
The DOT Calculus (Dependent Object Types) Nada Amin Scala Days June 18, 2014 1 DOT: Dependent Object Types I DOT is a core calculus for path-dependent types. I Goals I simplify Scala’s type system by desugaring to DOT I simplify Scala’s type inference by relying on DOT I prove that DOT is type-safe 2 Types in Scala and DOT 3 Types in Scala modular named type scala.collection.BitSet compound type C
Tagless-Final Style
The so-called ``tagless-final'' style is a method of embedding domain-specific languages (DSLs) in a typed functional host language such as Haskell, OCaml, Scala or Coq. It is an alternative to the more familiar embedding as a (generalized) algebraic data type. It is centered around interpreters: Evaluator, compiler, partial evaluator, pretty-printer, analyzer, multi-pass optimizer are all interpr
静的型チェックがあったらテストはあまり書かなくて良いのか - $shibayu36->blog;
昔に動的言語だとひたすらテストを書かないといけないけど、静的型チェックの仕組みがあればそんなにテストを書かなくてもいいよねみたいな話があった記憶がある。昔は結局どうなんだろうと思ってたのだけど、最近もそういう話を耳にして、やっぱりそんなことないだろうという気持ちになったのでメモ。ふと思いついただけなので正当性は分からない。 まずなぜそのような話になるのか考えたのだけど、「静的言語ならコンパイル時に型チェックをすることができるため安全性を高められる」という点からこういう話が上がってきているように思う。しかしよく考えてみると、静的型チェックという仕組みは、プログラムテキストとして正当であるかという点しか保証していない。つまり、特定の変数が必ずその型であるとか、特定のエンティティからのメソッド呼び出しが正しいか(メソッド名や引数など)とか、関数が返す型がかならず指定した型になるかとか、そのような
Write You a Haskell ( Stephen Diehl )
There is nothing more practical than a good theory. — James C. Maxwell Hindley-Milner Inference The Hindley-Milner type system ( also referred to as Damas-Hindley-Milner or HM ) is a family of type systems that admit the serendipitous property of having a tractable algorithm for determining types from untyped syntax. This is achieved by a process known as unification, whereby the types for a well-
Instances and Dictionaries - School of Haskell | School of Haskell
An Idealized Operational View of Type Class Dictionary PassingWhen you make a class class Foo a where quux :: a -> Int muux :: a -> Booland then an instance. data Bar = Bar instance Foo Bar where quux = \Bar -> 1 muux = \Bar -> TrueThere is a desugaring processes that occurs, removing type classes. For each class there is an associated record, data FooD a = FooD -- class Foo a where { quuxD :: a -
HaskellとOCamlの型の違い
Hideyuki Tanaka @tanakh 完全な型推論よりも、型システムの表現力が重要である、という考えは多分OCamlとは相容れない。そこがOCamlとHaskellの決定的な差であって、PureとかLazyとかの違いはそれに比べれば割りとどうでもいい。 2012-03-26 14:24:35 Jun Furuse 🐫🌴 @camloeba RT @tanakh 完全な型推論よりも、型システムの表現力が重要である、という考えは多分OCamlとは相容れない。そこがOCamlとHaskellの決定的な差であって、PureとかLazyとかの違いはそれに比べれば割りとどうでもいい。 2012-03-26 14:36:35
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
System F with type equality coercions - Microsoft Research
What is a nominal type?
Racket 6.11で篩型(refinement type)と依存関数型(dependent function type)が安定機能に
WTF is F-Bounded Polymorphism
https://okmij.org/ftp/tagless-final/course/lecture.pdf