Can strict ST break referential transparency?

Yuras Shumovich shumovichy at gmail.com
Tue Nov 21 18:00:52 UTC 2017


Sorry, link [2] meant to be
https://ghc.haskell.org/trac/ghc/ticket/11760

21-11-2017, Аўт а 20:43 +0300, Yuras Shumovich напісаў:
> Hello,
> 
> I was evaluating a possibility that linear types can break
> referential
> transparency [1], exactly like lazy ST [2].
> 
> But on the way I realized that even strict ST may suffer from the
> same
> issue. If ST computation is interrupted by e.g. async exception,
> runtime will "freeze" it at the point where it was interrupted [3].
> 
> So the question: is the "freezed" computation just a normal thunk?
> Note
> that the runtime doesn't guarantee that a thunk will be evaluated
> only
> once [4]. If the "freezed" thunk captures e.g. STRef, and will be
> evaluated twice, its effect could become observable from outside,
> just
> like in case of lazy ST.
> 
> I tried to check the theory by stress testing RTS. Unfortunately I
> immediately discovered a runtime crash [5], which is probably not
> related to my question.
> 
> Hope someone will be able to clarify things for me.
> 
> Thanks,
> Yuras.
> 
> [1] https://github.com/ghc-proposals/ghc-proposals/pull/91#issuecomme
> nt
> -345553071
> [2] https://ghc.haskell.org/trac/ghc/ticket/14497
> [3] See section 8 there: https://www.microsoft.com/en-us/research/wp-
> co
> ntent/uploads/2016/07/asynch-exns.pdf
> [4] https://www.microsoft.com/en-us/research/wp-content/uploads/2005/
> 09
> /2005-haskell.pdf
> [5] https://ghc.haskell.org/trac/ghc/ticket/14497


More information about the ghc-devs mailing list