Re: [Haskell-cafe] Coding Standards (Coding Conventions)
On 5/28/07, Donald Bruce Stewart [EMAIL PROTECTED] wrote: pvolgger: I wonder if there are any Coding Standards or Coding Conventions for Haskell. Does anybody know something about it? We've collected some style guides on the wiki. You could also look at projects whose code you think is in good style. http://haskell.org/haskellwiki/Category:Style GHC has a style guide. Our small little window manager, xmonad, also has a pretty strict style guide. Pugs has a style described here: http://svn.pugscode.org/pugs/docs/Pugs/Doc/Hack/Style.pod It recommends against punning datatypes and constructors, since we've noticed that confuses people reading the code. It also proposes a convention that minimizes clashes in field names. Pugs code tends to favor declarative over expression style and where over let. -- Gaal Yahas [EMAIL PROTECTED] http://gaal.livejournal.com/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Higher order types via the Curry-Howard correspondence
On 5/13/07, Josef Svenningsson [EMAIL PROTECTED] wrote: I think both Benja's and David's answers are terrific. Let me just add a reference. Yes, this entire thread has been quite illuminating. Thanks all! The person who's given these issues most thought is probably Per Martin-Löf. [...] In the beginning of the third lecture you will find the classic quote: the meaning of a proposition is determined by what it is to verify it, or what counts as a verification of it I like how this is reminiscent of Quine's ideas in On What There Is. Another reference to add is Simon Thompson, _Type Theory and Functional Programming_, which I stumbled upon online here: http://www.cs.kent.ac.uk/people/staff/sjt/TTFP/ . -- Gaal Yahas [EMAIL PROTECTED] http://gaal.livejournal.com/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Higher order types via the Curry-Howard correspondence
What do higher-order types like lists mean when viewed through the Curry-Howard correspondence? I've been wondering about this for a while. The tutorials ask me to consider id :: forall a. a - a (.) :: forall a b c. (b - c) - (a - b) - (a - c) These represent theorems in a logical calculus, with the variables a, b, c denoting propositions. In the case of the composition function, the proposition (a - c) may be deduced if (b - c) and (a - b) obtain, and so on. (I've obviously skimmed some details.) We know the function e :: a - b diverges because there is no way to deduce b from a with no other premises; the only value that satisfies this is bottom -- and so on. But what does the following mean? map :: (a - b) - [a] - [b] Since the empty list inhabits the type [b], this theorem is trivially a tautology, so let's work around and demand a non-trivial proof by using streams instead: data Stream a = SHead a (Stream a) sMap :: (a - b) - Stream a - Stream b What is the object Stream a in logic? What inference rules may be applied to it? How is data Stream introduced, and what about variant constructors? -- Gaal Yahas [EMAIL PROTECTED] http://gaal.livejournal.com/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
