4 ms·

Link to Simon PJ's own copy, with accurate extension: http://research.microsoft.com/en-us/um/people/simonpj/papers/state-lasc.ps.gz http://research.microsoft.c

Link to Simon PJ's own copy, with accurate extension: http://research.microsoft.com/en-us/um/people/simonpj/papers/state-lasc.ps.gz http://research.microsoft.com/en-us/um/people/simonpj/papers...

delackner 16y ago
I got to page 8, where he introduces an upside-down A as I guess a symbol meaning "the set of all" and do not understand even after three readings, anything that is said on page 9.
- celoyd 16y ago
  You guessed pretty much right: ∀ is usually read as for all. It and others he uses (like ⊢ for is derived from) are defined in http://en.wikipedia.org/wiki/List_of_logic_symbols http://en.wikipedia.org/wiki/List_of_logic_symbols . Hope that helps; as a beginner in Haskell and strong type systems, it looks like I’m going to have trouble with this too.
- ionfish 16y ago
  ∀ is the standard symbol for the universal quantifier: some proposition is true for all elements in the universe being quantified over. This is stated explicitly in the paper: "The type given for runST above is implicitly universally quantified over both s and a." We could thus expand the type given for runST as follows: runST is a function which, for every instance of the type a, and every instance of the type s, accepts a state transformer (with type ST s a) and returns a value of type a. If you want to attain a better understanding of the logical concepts and notation used in the article, try getting hold of an introductory logic text. I recommend Enderton's 'A Mathematical Introduction to Logic'. http://www.math.ucla.edu/~hbe/amil/index.html http://www.math.ucla.edu/~hbe/amil/index.html
  - delackner 16y ago
    Both your and the previous reply indicate that the blanks I filled in (the "for all" and "derived from" symbols) were indeed as I suspected, and yes I understood the definition of runST to be as you describe it. But I still don't comprehend their discussion of how defining runST thusly somehow provides safety in the example they say it would automatically detect is disallowed.

Link to Simon PJ's own copy, with accurate extension: http://research.microsoft.com/en-us/um/people/simonpj/papers/state-lasc.ps.gz http://research.microsoft.com/en-us/um/people/simonpj/papers...

delackner 16y ago

I got to page 8, where he introduces an upside-down A as I guess a symbol meaning "the set of all" and do not understand even after three readings, anything that is said on page 9.

celoyd 16y ago
You guessed pretty much right: ∀ is usually read as for all. It and others he uses (like ⊢ for is derived from) are defined in http://en.wikipedia.org/wiki/List_of_logic_symbols http://en.wikipedia.org/wiki/List_of_logic_symbols . Hope that helps; as a beginner in Haskell and strong type systems, it looks like I’m going to have trouble with this too.
ionfish 16y ago
∀ is the standard symbol for the universal quantifier: some proposition is true for all elements in the universe being quantified over. This is stated explicitly in the paper: "The type given for runST above is implicitly universally quantified over both s and a." We could thus expand the type given for runST as follows: runST is a function which, for every instance of the type a, and every instance of the type s, accepts a state transformer (with type ST s a) and returns a value of type a. If you want to attain a better understanding of the logical concepts and notation used in the article, try getting hold of an introductory logic text. I recommend Enderton's 'A Mathematical Introduction to Logic'. http://www.math.ucla.edu/~hbe/amil/index.html http://www.math.ucla.edu/~hbe/amil/index.html
- delackner 16y ago
  Both your and the previous reply indicate that the blanks I filled in (the "for all" and "derived from" symbols) were indeed as I suspected, and yes I understood the definition of runST to be as you describe it. But I still don't comprehend their discussion of how defining runST thusly somehow provides safety in the example they say it would automatically detect is disallowed.