[ Content | View menu ]

Developing Programs and Proofs Spontaneously using GADT

August 6, 2007

I am curious about the possibility of developing Haskell programs spontaneously with proofs about their properties and have the type checker verify the proofs for us, in a way one would do in a dependently typed language. I tried to redo part of the merge-sort example in Altenkirch, McBride, and McKinna’s introduction to Epigram: deal the input list into a binary tree, and fold the tree by the function merging two sorted lists into one.

[More ...] - 3 Comments
Tags: , , , , .

Encoding Inductive and Coinductive Types in Polymorphic Lambda Calculus

July 27, 2007

An indcutive type μF is simulated by forall x . (F x -> x) -> x, while a coinductive type νF is simulatd by exists x . (x -> F x, x). When they coincide, we can build hylomorphisms, but also introduces non-termination into the language.

[More ...] - 0 Comments
Tags: , , .

Polymorphic Types in Haskell without Constructors?

June 30, 2007

I was trying to simulate church numerals and primitive recursion in second rank polymorphism of Haskell. However, polymorphic types in Haskell can only be instantiated with monomorphic types.

[More ...] - 0 Comments
Tags: , .

Substraction not Definable in Simply Typed Lambda Calculus

June 21, 2007

We can even define primitive recursion, only that it does not have the desired type primrec :: (N -> b -> b) -> b -> N -> b. Therefore, predecessor does not get the type pred :: N a -> N a either.

[More ...] - 0 Comments
Tags: , .