Tag Archives: Types

Developing Programs and Proofs Spontaneously using GADT

By Shin | Published: 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.
Posted in Research Blog | Also tagged , , , | 3 Comments

Encoding Inductive and Coinductive Types in Polymorphic Lambda Calculus

By Shin | Published: 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.
Posted in Research Blog | Also tagged , | Leave a comment

Polymorphic Types in Haskell without Constructors?

By Shin | Published: 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.
Posted in Research Blog | Also tagged | Leave a comment

Substraction not Definable in Simply Typed Lambda Calculus

By Shin | Published: 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.
Posted in Research Blog | Also tagged | Leave a comment