Apfelmus,
Types like () or Int do not have a logical counterpart in
propositional logic, although they can be viewed as a constant
denoting
truth. In other words, they may be thought of as being short-hand for
the type expression (a,a) (where a is a fresh variable).
Could you explain this?
Apfelmus,
System F is closest to Haskell and corresponds to a second order
intuitionistic propositional logic (?).
Not propositional of course, but second-order indeed.
Not sure, what I meant there :-S. Please ignore it. You're right of
course: second-order intuitionistic propositional
Stefan Holdermans wrote:
Apfelmus,
Types like () or Int do not have a logical counterpart in
propositional logic, although they can be viewed as a constant denoting
truth. In other words, they may be thought of as being short-hand for
the type expression (a,a) (where a is a fresh variable).
Gaal Yahas wrote:
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
[...]
But what does the following mean?
map :: (a - b) - [a] - [b]
Since the empty list inhabits
Gaal Yahas gaal at forum2.org writes:
What do higher-order types like lists mean when viewed through the
Curry-Howard correspondence?
Okay well I don't know the complete answer, but since no one else has answered
I'll have a go.
Suppose we define our own version of list as
data List a =
