On Tue, Dec 20, 2011 at 17:52, Jesse Schalken <jesseschalken@gmail.com> wrote:
On Wed, Dec 21, 2011 at 1:09 AM, Gregory Crosswhite <gcrosswhite@gmail.com> wrote:
That would certainly be a lovely idea *if* we were programming in Agda, but I was under the assumption that this conversation was about Haskell.  :-)

I don't have experience with proof assistants, but maybe my answer to this thread can be summed up as giving Haskell that kind of capability. ;) 

You want to look at Agda:  a proof assistant language whose syntax is similar to Haskell, and which supports dependent types and the like.

--
brandon s allbery                                      allbery.b@gmail.com
wandering unix systems administrator (available)     (412) 475-9364 vm/sms