| ▲ | sourdecor a day ago | |
Could someone compare this to ST in Idris? | ||
| ▲ | throwaway17_17 a day ago | parent | next [-] | |
If you are asking in the context of Idris 2.0 (the current version), ST is not really related. However, if you mean ST in Idris 1.0, there is a definite correlation. The mechanism that ST used for enabling local mutations was very similar to the mechanism that the typestate pattern in Rust is using. ST was a framework for formalizing State Machines in dependent types which is the mechanism TFA is analyzing. | ||
| ▲ | vatsachak a day ago | parent | prev | next [-] | |
This is not really ST. This is analogous to eating at an old school restaurant. You can't just walk in to the food service counter and say "give me a burger"; you need to first get a ticket from the cashier proving that you've ordered a burger and then provide that ticket to the guy at the counter. That's literally the type state pattern | ||
| ▲ | nvader a day ago | parent | prev [-] | |
Yes, I believe it should be possible for someone to do that. | ||