[Haskell] Probably a trivial thing for people knowing Haskell

[Brandon S. Allbery KF8NH]

On 2008 Oct 19, at 11:24, Friedrich wrote:
> "Brandon S. Allbery KF8NH" <allbery at ece.cmu.edu> 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] allbery at kf8nh.com
system administrator [openafs,heimdal,too many hats] allbery at ece.cmu.edu
electrical and computer engineering, carnegie mellon university    KF8NH