Gaal Yahas 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 = Nil |
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 li
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 v
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 log