5 ms·

> Some aspects, as in: not possible to describe state machines by types. I really don't understand this, I mean: data TrafficLight = Red Int

> Some aspects, as in: not possible to describe state machines by types. I really don't understand this, I mean: data TrafficLight = Red Int | Green Int | Yellow (let's assume that you have a flexible traffic control system which permits chaning the duration of Red/Green due to live traffic data, but Yellow must always be, say, 5 seconds because the safety requirements say so.) Add a function nextState :: Input -> State -> State nextState = ... and you're done. Am I missing something? EDIT: Oh, I think I see what you're saying. This doesn't provide that many guarantees at the type level about state transitions, but I'd counter that: a) You have other options than "Int", so you could manage valid states more strictly, and b) There's such a thing as Dependently-Typed languages, say Idris, so you can go even further. Then, perhaps Dependently-Types languages was what you meant by "active subject of research". I'd probably agree on that :) > Add asynchrony in the equation and you're out of luck. Not sure how that's to be interpreted? Are you talking about asynchronous updates to state, or...? > And transducers can also have asynchronous behavior. Is there a formal description of what semantics they have in that scenario? Or are we just going by implementation details? EDIT: I should say: I'm not being faceitous or going for any kind of 'gotcha' type thing here. I'm really curious; maybe I'm just misunderstanding your post.

mac01021 10y ago
I'm as clueless as you are about that asynchrony business, but would like to point out that you are not fully describing your state machine within the type system unless the typechecker prohibits you from defining (nextState Yellow == Green).
- lomnakkus 10y ago
  That would be an invalid definition since you must provide an (integer) parameter to Green. Effectively you must "magic" a default value for what happens when Yellow goes to Green. (Obviously in my sketched scenario the value would really come from Input.)
  - mac01021 10y ago
    That's true. My point was just that your type definition does not tell the compiler/typechecker that the light, if it is currently yellow, must become red before it can become green. That's a rule of the state machine and, if the compiler doesn't stop you from writing a function that breaks that rule then your state machine has not been modeled fully within the type system. I'm pretty sure this is what Hickey et al mean when they say that Haskell's type system is not powerful enough to describe a state machine.
    - lomnakkus 10y ago
      > That's true. My point was just that your type definition does not tell the compiler/typechecker that the light, if it is currently yellow, must become red before it can become green. Ah, yes, I understand what you mean now, but you can actually encode that if you really want to. (If we assume Haskell, there's very limited DT programming which will probably let you state which transitions are legal. I must admit I'm not very up-to-speed on it, but see the next paragraph.) The thing is that people usually don't want to go that far. Whether you're working in a typed scenario or not. In the unityped scenario, you can't go that far without reinventing a (run-time?) type-checker. > That's a rule of the state machine and, if the compiler doesn't stop you from writing a function that breaks that rule then your state machine has not been modeled fully within the type system. > I'm pretty sure this is what Hickey et al mean when they say that Haskell's type system is not powerful enough to describe a state machine. Certainly this is true, but if you're in an entirely unityped setting... do you have any guarantees? (To which the answer is, of course, "no".) Foregoing all guarantees just because you can't guarantee everything seems... rash. (I believe this is the position that Hickey takes, for better or worse.) Obviously, that's why I, personally, prefer languages with multiple types. Note: I do think there are geniune scenarios where unityped may win out, e.g. "generic data transformation without knowing anything about the structure", but there's even "typed" answers for that, e.g. lenses. For my money -- and I'm obviously semi-joking -- ekmett >> hickey :)
      - tree_of_item 10y ago
        > Certainly this is true, but if you're in an entirely unityped setting... do you have any guarantees? This is what clojure.spec is all about. The answer is not, of course, "no". They are "reinventing a run-time type checker" and prefer it that way because it allows increased expressive power at the cost of delayed verification. > Ah, yes, I understand what you mean now, but you can actually encode that if you really want to. (If we assume Haskell, there's very limited DT programming which will probably let you state which transitions are legal. I must admit I'm not very up-to-speed on it, but see the next paragraph.) So you don't actually know how to do it, but assume that you can. This a little strange. Are you sure that "people usually don't want to go that far"? Because the real answer is probably "it's too hard to do". By the way, you probably want linear types in order to encode state machines in the type system in a natural way, which Haskell does not have.

mac01021 10y ago

I'm as clueless as you are about that asynchrony business, but would like to point out that you are not fully describing your state machine within the type system unless the typechecker prohibits you from defining (nextState Yellow == Green).

lomnakkus 10y ago
That would be an invalid definition since you must provide an (integer) parameter to Green. Effectively you must "magic" a default value for what happens when Yellow goes to Green. (Obviously in my sketched scenario the value would really come from Input.)
- mac01021 10y ago
  That's true. My point was just that your type definition does not tell the compiler/typechecker that the light, if it is currently yellow, must become red before it can become green. That's a rule of the state machine and, if the compiler doesn't stop you from writing a function that breaks that rule then your state machine has not been modeled fully within the type system. I'm pretty sure this is what Hickey et al mean when they say that Haskell's type system is not powerful enough to describe a state machine.
  - lomnakkus 10y ago
    > That's true. My point was just that your type definition does not tell the compiler/typechecker that the light, if it is currently yellow, must become red before it can become green. Ah, yes, I understand what you mean now, but you can actually encode that if you really want to. (If we assume Haskell, there's very limited DT programming which will probably let you state which transitions are legal. I must admit I'm not very up-to-speed on it, but see the next paragraph.) The thing is that people usually don't want to go that far. Whether you're working in a typed scenario or not. In the unityped scenario, you can't go that far without reinventing a (run-time?) type-checker. > That's a rule of the state machine and, if the compiler doesn't stop you from writing a function that breaks that rule then your state machine has not been modeled fully within the type system. > I'm pretty sure this is what Hickey et al mean when they say that Haskell's type system is not powerful enough to describe a state machine. Certainly this is true, but if you're in an entirely unityped setting... do you have any guarantees? (To which the answer is, of course, "no".) Foregoing all guarantees just because you can't guarantee everything seems... rash. (I believe this is the position that Hickey takes, for better or worse.) Obviously, that's why I, personally, prefer languages with multiple types. Note: I do think there are geniune scenarios where unityped may win out, e.g. "generic data transformation without knowing anything about the structure", but there's even "typed" answers for that, e.g. lenses. For my money -- and I'm obviously semi-joking -- ekmett >> hickey :)
    - tree_of_item 10y ago
      > Certainly this is true, but if you're in an entirely unityped setting... do you have any guarantees? This is what clojure.spec is all about. The answer is not, of course, "no". They are "reinventing a run-time type checker" and prefer it that way because it allows increased expressive power at the cost of delayed verification. > Ah, yes, I understand what you mean now, but you can actually encode that if you really want to. (If we assume Haskell, there's very limited DT programming which will probably let you state which transitions are legal. I must admit I'm not very up-to-speed on it, but see the next paragraph.) So you don't actually know how to do it, but assume that you can. This a little strange. Are you sure that "people usually don't want to go that far"? Because the real answer is probably "it's too hard to do". By the way, you probably want linear types in order to encode state machines in the type system in a natural way, which Haskell does not have.