Difference between revisions of "User talk:Gleb"
Jump to navigation
Jump to search
| (2 intermediate revisions by the same user not shown) | |||
| Line 1: | Line 1: | ||
| − | [[Category:Tutorials]] |
||
| − | == What does runST's type really mean == |
||
| − | This page is the result of short but insightful discussion on Haskell IRC channel (thanks mnislaih, malcomw, swiert and dons), it was suggested by Don Stewart (dons) to publish it. |
||
| − | |||
| − | Haskell's type system is cool, Haskell's type system is sexy, it allows expressing quite complex constraints and program properties not expressible in other languages' type systems. But there's downside to it: types involving various extensions like higher-rank polymorphism can be quite difficult to comprehend. While it is useful an may be even necessary to have a good grasp of intuitionistic logic, Curry-Howard isomorphism and theoretical foundations of Computer Science in general for mastering type-level hackery, it may be helpful, especially for newbie programmers, to have some intuitive way of reading "sexy" types without having to understand how Haskell's type inference and type checking works. |
||
| − | |||
| − | Consider <hask>ST</hask> monad and the <hask>runST</hask> function. <hask>ST</hask> actions, like <hask>State</hask> actions, |
||
| − | are indexed by <hask>s</hask> type variable, but analogy between <hask>ST</hask> and <hask>State</hask> can be misleading. <hask>State</hask> monad is parametrised by user, and <hask>s</hask> is instantiated with some concrete type. For example, <hask>State Int String</hask> is a type of stateful computation that mutates hidden variable of type <hask>Int</hask> and returns <hask>String</hask>. |
||
| − | |||
| − | It's less clear though what type variable <hask>s</hask> denotes in the type <hask>ST s a</hask> and why <hask>runST</hask> has the type <hask>(forall s . ST s a) -> a</hask>. |
||
| − | |||
| − | Original [http://citeseer.ist.psu.edu/launchbury94lazy.html article] on ST monad says: |
||
| − | |||
| − | ''...Now, what we really want to say that runST should only be applied to a state transformer which uses newVar to create any references which are used in that thread. To put it in anouther way, the argument of runST should not make any assumptions about what has already allocated in the initial state. That is, runST should work regardless of what initial state is given. ...'' |
||
| − | </quote> |
||
| − | |||
| − | The article further explains how leaking mutable references like <hask>runST (newVar True)</hask> is rejected by typechecker due to escaping type variable. |
||
| − | |||
| − | In my opinion, the most intuitive explanation of <hask>ST</hask> actions' types was suggested by mnislaih: |
||
| − | |||
| − | |||
| − | ''Maybe it helps to think that in the type <hask>ST s a</hask>, <hask>s</hask> models the state thread, and every time you make a new <hask>STRef</hask>, it becomes tied to a given state thread. So one can say that the domain of <hask>s</hask> is the domain of state threads |
||
| − | '' |
||
| − | |||
| − | Since I could have distorted some of ideas that guys on IRC channel tried to convey, the following is the log of IRC conversation: |
||
| − | |||
| − | ---- |
||
| − | |||
| − | [13:01] gleb: hello everyone. i have a bit philosophical, perhaps a bit silly question, but anyway. is there some mnemonic, some intuitive way to read types of higher-rank polymorphic functions? consider for instance runST :: (forall s. ST s a) -> a. I understand that runST has this type because STRef's aren't allowed to escape. i've read and kind of understood the explanation of how things like 'runST (newSTRef True)' are rejected by typechecker because of escaping type variable 's'. but |
||
| − | |||
| − | [13:01] gleb: my point is that usually one doesn't have to understand how typechecker works to understand the type. Types like (id :: a->a) or (put :: (MonadState s m) => s -> m ()) make a lot more sense because every type variable actually denotes something, and in the type (ST s a) it doesn't. thanks. |
||
| − | |||
| − | [13:03] dons: gleb: hmm. good question. |
||
| − | |||
| − | [13:04] gleb: dons: i'm glad you think it is |
||
| − | |||
| − | [13:04] dons: gleb: so its all in the scoping of the type variables, but i don't have an intuitive way to read that. |
||
| − | |||
| − | [13:04] dons: gleb: i'd even be inclined to ask on haskell-cafe@ to see if someone has a nice intuition |
||
| − | |||
| − | [13:04] gleb: dons: ok, i'll post my question to cafe |
||
| − | |||
| − | [13:05] mnislaih reads that as "for any ST action where s is free" |
||
| − | |||
| − | [13:06] dons: that's a good way to think about it, mnislaih |
||
| − | |||
| − | [13:06] mnislaih: one needs to know that STRefs bind s to something in order to make any sense |
||
| − | |||
| − | [13:07] malcolmw: the (forall s . ST s a) reads to me that the state parameter given to ST is internal, because nothing can influence what the s is from outside |
||
| − | |||
| − | [13:07] malcolmw: it must "work", for any given 's' |
||
| − | |||
| − | [13:07] malcolmw: (and therefore we don't give an 's' at all!) |
||
| − | |||
| − | [13:08] swiert: gleb: I sometimes find it helpful to think about how it all boils down to System F - where types are instantiated explicitly. |
||
| − | |||
| − | [13:09] swiert: I'm not sure if that helps you though. |
||
| − | |||
| − | [13:09] mnislaih: malcolmw the "it must work for any given s" intuition works for me with dimensions, i.e. for matrix computations where dimensions appear in the type. But it doesn't help me with ST |
||
| − | |||
| − | [13:11] gleb: swiert, mnislaih, malcolmw: thanks for sharing your intuitions, but they really require knowing 'how typechecker works', what i've mentioned in my question |
||
| − | |||
| − | [13:11] dons: gleb: yes, that *really* helps. writing a little type checker for Hindley-Milner is a very useful learning exercise |
||
| − | |||
| − | [13:12] malcolmw: gleb: I don't agree, I think of it entirely in terms of predicate calculus |
||
| − | |||
| − | [13:13] malcolmw: gleb: the type signature is stating a logical property, involving constraints on the domains and ranges of values, and quantification is a natural part of the specification for more complicated properties |
||
| − | |||
| − | [13:14] gleb: ok, let's put it another way. consider a haskell newbie that just mastered State monad and is trying to understand ST monad. they appear somewhat analogous in their purpose, ST being more rich and sophisticated. types State s a and ST s a look similar. how would you explain to a newbie, what s means in the type of ST s a? |
||
| − | |||
| − | [13:15] malcolmw: gleb: in State s a, the user provides the state. In ST s a, the system provides it (opaquely), so you are not allowed to assume anything about what it looks like |
||
| − | |||
| − | [13:17] mnislaih: gleb: I don't see another way apart from teaching gim about rank-2 types |
||
| − | |||
| − | [13:17] malcolmw: and indeed, there are only very few things you can do with the state in ST s a, namely reading and writing STRefs - that's all |
||
| − | |||
| − | [13:17] mnislaih: him/her |
||
| − | |||
| − | [13:19] gleb: malcolmw: i like your point about logical properties. afaik variables in predicate calculus range over some domain, and statements like forall x . Human(x) -> Mortal(x) can be translated to natural language |
||
| − | |||
| − | [13:19] gleb: the question is what is the domain of 's' in ST s a? |
||
| − | |||
| − | [13:19] malcolmw: gleb: exactly |
||
| − | |||
| − | [13:20] malcolmw: gleb: but in the type system, domains are explicit, e.g. Int, and variables are polymorphic, meaning "give me some domain, any domain" |
||
| − | |||
| − | [13:21] malcolmw: gleb: so a type variable has the domain of "all possible types" |
||
| − | |||
| − | [13:23] malcolmw: gleb: at runtime, of course, the type variable must be instantiated to some particular types, |
||
| − | |||
| − | [13:24] malcolmw: (conceptually, anyway, since there are no type representations at runtime, to a first approximation) |
||
| − | |||
| − | [13:24] mnislaih: maybe it helps to think that in the type ST s a, s models the state thread, and every time you make a new STRef, it becomes tied to a given state thread. So one can say that the domain of s is the domain of state threads |
||
| − | |||
| − | [13:25] gleb: mnislaih: thanks! that is nice intuition |
||
| − | |||
| − | [13:25] malcolmw: I would say that it is more about "who gets to instantiate this type variable". For normal polymorphic variables, it is the caller of the function that instantiates them to some particular type |
||
| − | |||
| − | [13:26] malcolmw: but in the (forall s . ....) bracket, it prevents the caller from being able to see the variable s, so it |
||
| − | cannot be instantiated by the calling context |
||
| − | |||
| − | [13:26] gleb: malcolmw: but as far as i understand, 's' is never instantiated |
||
| − | [13:26] mnislaih: gleb that's what malcolmw is saying. In fact, the domain of s is any type. But it helps to think that it is |
||
| − | the state thread |
||
| − | |||
| − | [13:27] malcolmw: gleb: oh, it _is_ instantiated, but internally and opaquely by the implementation |
||
| − | |||
| − | [13:27] Saizan: gleb: it's instantiated by runST effectively, it's fixed to some particular "s" so that you can't mix it with |
||
| − | a different one |
||
| − | |||
| − | [13:28] gleb: guys, thanks a lot. this discussion was really enlightening |
||
| − | |||
| − | [13:28] mnislaih: malcolmw: that would be only to RealWorld in IO. Saizan, for that matter, it is never instantiated. It is kept free |
||
| − | </quote> |
||
| − | |||
| − | --[[User:Gleb|Gleb]] 23:05, 7 June 2007 (UTC) |
||