Records are Sheaves of Types
Records are Sheaves of Types. Let us define a record type as being given by a type \(X\) of keys and an interpretation function \(F\) which maps every key \(x:X\) to a type. We assume the existence of a powerset functor \(\mathcal{P}: \mathbf{Type}\to\mathbf{Type}\) , which endows the discrete topology on \(X\) . Then a record type is the product of the image of \(F\) over a subset of \(X\) : \[ \
JS ⊢ Dependent Types for Pragmatics
I am pleased to make available the result of joint research with Darryl McAdams, our new paper Dependent Types for Pragmatics which is currently under review for publication in the Journal of Logic, Language and Information. I’d like to discuss a few aspects of the work which I consider important, lending additional emphasis to foundational aspects of type theory which I fear were lost in the pres
JS ⊢ Programming in Vinyl (BayHac 2014 Slides & Video)
Programming in Vinyl (BayHac 2014 Slides & Video). I lectured on Vinyl and its denotation in Type Theory at BayHac. Slides are available here, and there is a (screen) video of the presentation here. Among other things, I presented my new idea for records as sheaves, and my setting of Vinyl-style records in the context of the existing Containers research. Want to comment? I’m @jonsterling on Twitte
Jonathan Sterling – Vinyl: Modern Records for Haskell
Vinyl is a general solution to the records problem in Haskell using type level strings and other modern GHC features, featuring static structural typing (with a subtyping relation), and automatic row-polymorphic lenses. All this is possible without Template Haskell. First, install Vinyl from Hackage: cabal update cabal install vinyl Let’s work through a quick example. We’ll need to enable some lan
Jonathan Sterling – Dependent Types Today: Faking It With Style
There have been various attempts at faking dependent types in Haskell, most notably Conor McBride’s Strathclyde Haskell Enhancement. Since its creation, several improvements to GHC have set the stage for some of SHE’s features to be implemented natively. Let’s see what’s necessary to fake dependent types with singletons in today’s GHC. First, the usual boilerplate: > {-# LANGUAGE NoMonomorphismRes
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
JS ≫ Some Remarks on Dialectics in Mathematics
JS ⊢ Programming in Vinyl (BayHac 2014 Slides & Video)
JS ⊢ Standard ML as a Proof System, without GADTs
Jonathan Sterling – Proving Type Inequality in C++
Jonathan Sterling – Pi & Sigma: Adding Universe Polymorphism
Jonathan Sterling – Indexed Free Monads: Length-Typed Vectors for Free