On 2008 Oct 19, at 11:24, Friedrich wrote:
"Brandon S. Allbery KF8NH" <[EMAIL PROTECTED]> writes:
The relationship
between types and proofs is especially obvious in Haskell. And
proofs
aren't merely mathematical entities, they're expressions of what you
want to accomplish: if you can type your program, you have a high
likelihood not only that it will compile, but that it will do what
you
intend.
Well I could argue with the types in C and would not come along very
far. In the TCP/IP stuff one can see what you have to do, sooner or
From a Haskell standpoint, C and Java are virtually untyped.
If you want to see types => programs in action, play around with the
@free and @djinn commands in lambdabot (a Haskell bot that lives on
FreeNode). @free treats a type as a theorem and produces a "proof" of
it in Haskell code; @djinn takes a function declaration (type -> type)
and generates the "obvious" code suggested by the declaration.
(@djinn is sadly somewhat limited; it doesn't handle recursive types,
so e.g. lists don't work too well.)
--
brandon s. allbery [solaris,freebsd,perl,pugs,haskell] [EMAIL PROTECTED]
system administrator [openafs,heimdal,too many hats] [EMAIL PROTECTED]
electrical and computer engineering, carnegie mellon university KF8NH
_______________________________________________
Haskell mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell
