
Recent Posts
Recent Comments
sanjoyd on Faking Dependent Types in… drocta on Faking Dependent Types in… Matt on Faking Dependent Types in… Francis Kim on Faking Dependent Types in… Anurag Bishnoi on On why religion is a double… Archives
Categories
Meta
Tag Archives: haskell
Classical Axioms in Coq
For the past few days I’ve been working through an amazing text, Software Foundations, which aims to develop “basic concepts of functional programming, logic, operational semantics, lambdacalculus, and static type systems, using the Coq proof assistant”. This post is an … Continue reading
Posted in Computers
Tagged agda, cic, classical logic, coq, haskell, logic, theorem proving
Leave a comment
Typechecking TAL0 in Agda.
This post is an annotated solution to problem 4.2.11 in the book Advanced Topics in Types and Programming Languages from the chapter Typed Assembly Language by Gerg Morrisett. Introducing TAL0 I’ll do my best to give an informal introduction to … Continue reading
Posted in Computers
Tagged agda, function programming, haskell, static analysis, TAL, typed assembly, types
Leave a comment
Initial Algebras: Part II
In the last post we looked at functor algebras and properties of morphisms (arrows) between them. In this post we’ll explore initial functor algebras (or initial FAlgebras). The Cliffhanger The last episode ended with a question on whether it is … Continue reading
Posted in Computers
Tagged category theory, computer science, haskell, math, Programming
Leave a comment
Initial Algebras: Part I
Metapost This post is light on math and uses Haskell to express formalisms. If you’re clear on what a Functor is, you’re good to go. Functors and Algebras There is this regular old functor, with the type constructor Func. We’ve … Continue reading
Posted in Computers
Tagged arrows, category theory, functional programming, functors, haskell, initial algebra
6 Comments
Logic Puzzles in Agda
This post assumes basic knowledge of Agda. A few days ago, Paul Snively published a post which set me thinking on how Agda (which is the closest thing to Coq I have some knowledge of) fares in similar scenarios. Pretty … Continue reading
First steps with Agda: provable factoring
In my last post we looked at the problem of factoring an integer. We ran into an issue with the termination checker and resolved it by wrapping the recursion into a separate inductive datatype that made it explicit. The idiom … Continue reading
TypeSafe Tictactoe
I recently had occasion to screw around Haskell’s type system. The end goal was to produce a Tictactoe game in which all typecorrect moves are legal and where all illegal moves produce type errors. I decided call the following moves … Continue reading