Category Archives: Research Blog

Agda Exercise: Proving that Mergesort Returns Ordered Lists

By Shin | Published: September 28, 2007

This time I am implementing the example in another section of Why Dependent Types Matter by Altenkirch, McBride, and McKinna in Agda: proving that mergesort returns an ordered list.

Posted in Research Blog | Tagged , | 2 Comments

Agda Exercise: Sized Mergesort

By Shin | Published: September 27, 2007

Continuing with my Adga programming practice. Part of the mergesort example became easy once Max showed me how I should perform the pattern matching in insert.

Posted in Research Blog | Tagged , | 4 Comments

My First Agda Program: Append, Reverse, and Merge

By Shin | Published: September 19, 2007

During the WG 2.1 meeting, my attention was brought to Agda. So, here is my first Agda program. I am merely repeating some simple exercises on lists, which I tried using Haskell in a previous entry Developing Programs and Proofs Spontaneously using GADT.

Posted in Research Blog | Tagged , , | 2 Comments

An Unsuccessful Attempt to Compute the Intersection of Regular Expressions

By Shin | Published: August 9, 2007

Tyng-Ruey, Chin-Lung, and I needed to compute the intersection of two regular expressions without converting them to finite automata. The result was not satisfactory, however.

Posted in Research Blog | Tagged | 2 Comments

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 | 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 | Tagged , , | Leave a comment

Proving Some Equalities in Propositional Logic

By Shin | Published: July 2, 2007

Proving De Morgan’s laws and the double negation law in boolean algebra. Notes taken while listening to Max’s course on logic.

Posted in Research Blog | 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 | 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 | Tagged , | Leave a comment

Zipping Half of a List with Its Reversal

By Shin | Published: June 20, 2007

Given a list, zip its first half with the reverse of its second half, in only “one and a half” traversals of the list.

Posted in Research Blog | Tagged , | 4 Comments