<html><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; "><br><div><div>On Jun 26, 2010, at 11:21 AM, Andrew Coppin wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite"><span class="Apple-style-span" style="border-collapse: separate; color: rgb(0, 0, 0); font-family: Helvetica; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; orphans: 2; text-align: auto; text-indent: 0px; text-transform: none; white-space: normal; widows: 2; word-spacing: 0px; -webkit-border-horizontal-spacing: 0px; -webkit-border-vertical-spacing: 0px; -webkit-text-decorations-in-effect: none; -webkit-text-size-adjust: auto; -webkit-text-stroke-width: 0px; font-size: medium; "><blockquote type="cite">A first order logic quantifies over values, and a second order logic quantifies over values and sets of values (i.e., types, predicates, etc). &nbsp;The latter lets you express things like "For every property P, P x". &nbsp;Notice that this expression "is equivalent" to Haskell's bottom type "a". &nbsp;Indeed, Haskell is a weak second-order language. Haskell's language of values, functions, and function application is a first-order language.<br></blockquote><br>I have literally no idea what you just said.<br><br>It's like, I have C. J. Date on the shelf, and the whole chapter on the Relational Calculus just made absolutely no sense to me because I don't understand the vocabulary.</span></blockquote></div><br><div>Let's break it down then. &nbsp;A language is a set of "terms" or "expressions", together with rules for putting terms together (resulting in "sentences", in the logic vocabulary). &nbsp;A "logic" is a language with "rules of inference" that let you transform sets of sentences into new sentences.</div><div><br></div><div>Quantification is a tricky thing to describe. &nbsp;In short, if a language can "quantify over" something, it means that you can have variables "of that kind". &nbsp;So, Haskell can quantify over integers, since we can have variables like "x :: Integer". &nbsp;More generally, Haskell's run-time language quantifies over "values". &nbsp;</div><div><br></div><div>From this point of view, Haskell is TWO languages that interact nicely (or rather, a second-order language). &nbsp;First, there is the "term-level" run-time language. &nbsp;This is the stuff that gets evaluated when you actually run a program. &nbsp;It can quantify over values and functions. &nbsp;And we can express function application (a rule of inference to combine a function and a value, resulting in a new value).&nbsp;</div><div><br></div><div>Second, there is the type language, which relies on specific keywords:</div><div><br></div><div><font class="Apple-style-span" face="Courier">data, class, instance, newtype, type, (::)</font></div><div><br></div><div>Using these keywords, we can quantify over types. &nbsp;That is, the constructs they enable take types as variables.</div><div><br></div><div>However, notice that a type is "really" a collection of values. &nbsp;For example, as the Gentle Introduction to Haskell says, we should think of the type Integer as being:</div><div><br></div><div>data Integer = 0 | 1 | -1 | 2 | -2 | ...</div><div><br></div><div>despite the fact that this isn't how it's really implemented. &nbsp;The Integer type is "just" an enumeration of the integers.</div><div><br></div><div><br></div><div>Putting this all together and generalizing a bit, a second-order language is a language with two distinct, unmixable kinds variables, where one kind of variable represents a collection of things that can fill in the other kind of variable.</div><div><br></div></body></html>