Many thanks for answering my questions.
Actually, I am studiyng the paper
lazy functional state threads
in order to understand the runST function. That's where the type "State" comes from.
I have given a course in logic at the university of Burundi with mathematical set
theory as an application; I only needed one sort of variables to give to my students
the foundations of mathematics I also used an interesting construction of the
quantifier " there
exists x " that was based on Bourbaki's book : "Theory of sets".
I have some notes about lambda-calculus , but I have nothing about typed lambda
calculus.
Maybe you want to answer other questions as well.
1. In Haskell there are 2 sorts of variables : variables that range over values of a
specific type and "type variables".
e.g.in fact n = n * fact (n - 1) (the factorial function n ranges over the values
of type Int.
and in the type ST s a where s and a are variables that only range over
types
Am I correct?
2. I would first like to come back to the type signature
f :: a -> b
I can say the type of f is a -> b , isn't it? But a and b are both variables.
Question
can I replace the General type b by the type c -> d ?
then I would get that f is of type a-> (c -> d) which becomes (left associativity
of -> ) a -> c -> d.
After renaming my variables I get f is of type a -> b -> c
Wrong or right?
Friendly
Jan Brosius
