How Dependent Haskell Can Improve Industry Projects
Dependent types are a hot topic in the Haskell community. Many voices advocate for adding dependent types to Haskell, and a lot of effort is being invested towards that end. At the same time, the sceptics raise various concerns, one being that dependent types are more of a research project than a tool applicable in industrial software development. That is, however, a false dichotomy. While depende
GitHub - ollef/sixty: Dependent type checker using normalisation by evaluation
Surface syntax Core syntax Safe and fast phantom typed De Bruijn indices Evaluation Inlining of globals Readback Parsing Indentation-sensitivity Pretty printing Scope-aware name printing Unification and meta variables Pruning The "same meta variable" intersection rule Solution inlining Elaboration of meta variable solutions to local definitions Case expression inversion Basic type checking Elabora
Defunctionalization for the win
I enjoy using a type system to help make sure my term level code is unimpeachably correct. This is where my interest in writing the singletons library came from. This library allows you to write some dependently typed code in Haskell, using singleton types. I didn’t invent this idea, but I did write a nice library to remove some of the pain of using this encoding. SHE can be considered an ancestor
Why Dependent Haskell is the Future of Software Development
Hi, I’m Vladislav Zavialov. For the last couple of months, my job at Serokell has been to lead our efforts to improve our primary tool – the Glasgow Haskell Compiler (GHC). I’m focusing on making the type system more powerful, inspired by Richard Eisenberg’s thesis that introduces Dependent Haskell. Dependent types are a feature I’d love to see in Haskell the most. Let’s talk why. There’s a tensio
Abusing Haskell dependent types to make Redis queues safer
I don’t know about you, but quite frankly I’m tired of seeing the same tired vector example being used to demonstrate why dependent types are useful. Recently, I had the opportunity to use current Haskell’s dependently-typed facilities to solve a somewhat contrived, yet real-world problem. Below I will go through the steps I took in moving from an untyped free-for-all to having GHC reject more bad
依存型の紹介と応用としてのClashの紹介
目的 19番目の Advent Calender 2017 Haskell（その2）です。 依存型とは何か、何に役に立つのか、その応用としてのClashと Clashを用いた論理回路の実装のトライアルの紹介をします。 依存型とは何か Wikipediaの依存型のリンク先に他の型の値に依存する型が依存型とあります。例えば、Boolの値はTrue,Falseがありますが、Boolが型なのはもちろんですが、TrueやFalseも型として扱えるようになります。 その代表的なものとして、リストの要素数を埋め込んだ型があります。例えば、普通のBoolのリストは[Bool]な感じで長さに決まりはないですが、Vector 5 Boolのように長さ5のBool型のリストが作れます。(vector-sizedパッケージで実際に作れます。) 型に値を埋め込むだけだとありがたみがないですが、カリー＝ハワード同型対
Dependent Types in Haskell
Haskell Srbija Grupa posvećena ucenju i popularizaciji Haskell programskog jezika "Pure mathematics is, in its way, the poetry of logical ideas." Albert Einstein "Most good programmers do programming not because they expect to get paid or get adulation by the public, but because it is fun to program." Linus Torvalds This topic is considered as advanced and some prior knowledge of Haskell is assume
実世界を扱う依存型プログラミングのたぶん基本～外界から安全な世界までの道 - ぼくのぬまち 出張版
依存型ならさらに安全にプログラミングできちまうんだ！と言ったところで，「無料で遊べちまうんだ！」とか「3000円払えば無料で10連まわせる」みたいな感があり， 依存型使わない場合とどう違ってくるのか 入出力から扱い始めるとどういった形のプログラムになるのか 大概どういう流れでプログラミングすることになるのか とか，そういった話を通しではそんなに見ないかなーという気がしたので，ごく基本的なものを一通りまとめておこうと思って． まず，説明に使う問題設定について．行列演算，特に行列積を考えてみる．ただし，行列の形(行はいくつ，列はいくつ)についてはプログラムの外から入力によって決定するような状況とする．これ自体は普通の問題設定だと思われる． 依存型を使わなければ特にどうということも無い．恐らく行列の型を次のように定義し， -- 形のみ持っておき，中身の数値については簡単のため省略 data Ma
Dependent types in Haskell: Progress Report
It was drawn to my attention that there is an active Reddit thread about the future of dependent types in Haskell. (Thanks for the heads up, @thomie!) Instead of writing a long response inline in Reddit, it seems best to address the (very knowledgeable, respectful, and all around heartening) debate here. When can we expect dependent types in GHC? The short answer: GHC 8.4 (2018) at the very earlie
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
GitHub - vekatze/neut: A programming language with static memory management based on λ-calculus
HASKELLで依存型と コンパイル時 インラインLISP
GitHub - RyanGlScott/eliminators: Dependently typed elimination functions using singletons
GitHub - sweirich/corespec: A Specification for Dependent Types in Haskell (Core)
GitHub - ditto/ditto: A Super Kawaii Dependently Typed Programming Language