型安全なリストを作るのです(｀・ω・´) ～ その2、GADTsと依存型＞ω＜
前回のあらすじですー＞ω＜ Phantom Typeを駆使して空リストに適用しようとすると、コンパイル時にエラーを吐く型安全なリストを定義したのです(｀・ω・´) しかし、tailはよく分からないエラーに阻まれて定義することができなかったのです……＞＜; 今回は型安全なtailはどうやったら実現可能か考えてみたいと思いますです＞ω＜ 前回のエラーをもう一度確認してみますです。 前回のソースコードとエラーを再掲しておきますです(｀・ω・´) SafeList_by_PhantomType.hs{-# LANGUAGE ExistentialQuantification #-} module Main where import Prelude hiding (head, tail) data Empty data NonEmpty data SafeList x a = forall y. C
Part I: Dependent Types in Haskell - School of Haskell | School of Haskell
Interactive code snippets not yet available for SoH 2.0, see our Status of of School of Haskell 2.0 blog post In this series, we will see how to write dependently-typed programs and prove their correctness within haskell. At first, let's start with the standard example of Vector to understand how to write the dependently-typed programs in Haskell. The topic of this series is already implemented in
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
モナドとはモナドである - モナドとわたしとコモナド
この記事を読む前に、絶対に理解出来ないモナドチュートリアルに一度目を通してみてほしい。モナドを理解していく上で、とても重要なことが書かれている。 改めて言おう、モナドはモナドだ。コンテナだとかプログラマブルセミコロンだという説明では、モナドのすべてを正確に表せるとは言い難い。では、モナドを過不足なく説明できる、モナド以外の言葉はあるのか？ 実は、モナドを表現し、かつモナドで表現される言葉は存在する。その一つは手続きである。手続き型言語の「手続き」だ。 手続きとは何か 手続きは結果を持つ おおよそすべての手続きは何らかの結果を持つ。Haskellの()、C言語のvoid、PythonのNone、Rubyのnilなども結果の一種だ。結果が出ないとしたら、そのプログラムは停止しないか、途中で異常終了するだろう。 手続きには最小単位が存在する 処理系が扱っている以上、手続きが際限なく分解できるとい
型安全なリストに対する補足とGADTsの話ですー＞ω＜
お久しぶりですー＞ω＜ 気がついたら一ヶ月も経っていてしまいました(´・ω・｀) 前回の記事で実際に動かすことの出来ないtailを公開してしまったので、この記事はその謝罪と説明と補足になります(｀・ω・´) 前回の記事で問題だったところ(・ω・? 問題だったのは、具体的にはここですm9（・∀・）ﾋﾞｼｯ!! このtailは残念なことに型エラーが出て動かないのです(´・ω・｀) なぜなのでしょうか？？ 出てきたエラーメッセージを見てみます＞＜ SafeList_by_PhantomType.hs: Couldn't match type `y' with `x' `y' is a rigid type variable bound by a pattern with constructor Cons :: forall x a y. a -> SafeList y a -> SafeList
GADTs使ってみた - Faith and Brave - C++で遊ぼう
このエントリは、Haskell Advent Calendar 2011の参加記事です。 今回は、HaskellのGHC拡張であるGADTs(Generalized Algebraic Data Types : 一般化代数データ型)を調べて使ってみたという内容を書いてみました。 最初に、GADTsはGHC拡張なので、使用するには以下のようにして拡張を有効にする必要があります： {-#LANGUAGE GADTs #-} まずは構文的な違いを、Maybeを例にして見てみましょう。 通常の代数データ型では、Maybeは以下のように書きます： data Maybe a = Nothing | Just a GADTsでは以下のように書きます： data Maybe a where Nothing :: Maybe a Just :: a -> Maybe a 通常の代数データ型では、データコンス
Simon Peyton Jones先生招待講演について - Preferred Networks Research & Development
村主です。 ２０１１年９月２１日に、ICFP2011で来日していたSimon Peyton-Jones先生を弊社にお招きして、Glasgow Haskell Compilerの最新事情について講演をしていただきました。当日は体が浮きそうなほどの風が吹く大嵐でしたが、多くの人の協力のおかげで無事に終えることができ、感謝しています。 サイモン先生からスライドを分けてもらったので、講演会の動画とあわせて読む形で、記事にまとめてみました。Haskell/GHCのさまざまなトピックをカバーするこの講演、みなさんのHaskell勉強の一助となれば幸いです。 サイモン先生に「君たちも何か話してよ」と頼まれたので、僕が流体計算言語Paraiso(リンク先にスライドあり)の話をまずしています。 31:46 頃からサイモン先生のトークが始まります。まずはHaskell Communities and Acti
Haskell でダックタイピング 、色々な型を混ぜて配列を作る。 - 言語ゲーム
動的型言語の特徴の一つに、配列に色々な型のデータを混ぜられる事があります。いわゆるダックタイピングというやつです。例えば Javascript では ["1", 2, 3.4] のような配列を作る事が出来ます。Haskell のような強い型付けのある言語でこれを実現する方法を勉強したので書きます。 目標として、配列の中にあるデータを文字列として連結する事にします。Javascript で言うと、 append = function (xs) { var result = xs[0]; for (var i = 1; i < xs.length; i++) result += xs[i]; return result; } のような関数 append を作ります。append(["1", 2, 3.4]) の答えは "123.4" になります。 代数データ型を使う Haskell では直接リ
Type Families , Type Families (2) - #3(2009-09-07)
■ [Haskell] Type Families Data Familiesは、型パラメータに依って実装を変えたいときに使えます。C++のテンプレートでの特殊化みたいなものでしょうか*1。 {-# LANGUAGE TypeFamilies #-} import qualified Data.Sequence as Seq data family Vector a -- BoolのVectorはリストで表現 data instance Vector Bool = BoolVector [Bool] -- IntのVectorはSeqで表現 data instance Vector Int = IntVector (Seq.Seq Int) -- 関数はクラスにする必要があります class VectorElem a where add :: a -> Vector a -> Vector
Haskell+GADTで定理証明 その1: 型レベル自然数の等価性 - keigoiの日記
実は、私のfull-sessionsというセッション型のライブラリは中で unsafeCoerce#を使っているので型安全でない。使ってくれる人にとってそれは心もとないだろうし、そもそもunsafeなんとかは、いけがみさんによればSPJとSimon Marlowしか使ってはいけないことになっているらしい。やっぱりHaskellを使うものとして型安全性くらいは保証したい。でも、かといって普通のHaskellではうまく型を付けられない。(Typeableクラスのキャストを使っても解決にはならない。) そこで、魔法のGADT。 この型とこの型はぜったい等しいのにーというのが文脈から明らかなとき、それを表現できるのがGADTだ…というのが私の理解。まさしく私のケースにぴったりだ。これを使えばunsafeCoerceなんか要らんかもしれない。 いいかえれば、いわゆる定理証明をGADTつきのHaske
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
How wonderful to be (statically) typed 〜型が付くってスバラシイ〜
B-trees with GADTs – Matthew Brecknell
lucille development blog » Blog Archive » GADTs and Type Variables
Complete and Decidable Type Inference for GADTs