Closed jonsterling closed 8 years ago
Developing the denotational semantics of Dependent LCF has clarified things greatly, and now I know that the thing implemented here is not a monad, much less the "right" monad. It is, however, implementable in terms of the right thing.
The correct way to do Dependent LCF is given in this snippet: https://gist.github.com/jonsterling/6a8dfc6a36e5d6284d3d8204c7285de1
It is very simple! And there is no need for the relative monad apparatus here.
Developing the denotational semantics of Dependent LCF has clarified things greatly, and now I know that the thing implemented here is not a monad, much less the "right" monad. It is, however, implementable in terms of the right thing.
The correct way to do Dependent LCF is given in this snippet: https://gist.github.com/jonsterling/6a8dfc6a36e5d6284d3d8204c7285de1
It is very simple! And there is no need for the relative monad apparatus here.