{"action":"created","issue":{"url":"https://api.github.com/repos/jonsterling/tt-singletons/issues/2","labels_url":"https://api.github.com/repos/jonsterling/tt-singletons/issues/2/labels{/name}","comments_url":"https://api.github.com/repos/jonsterling/tt-singletons/issues/2/comments","events_url":"https://api.github.com/repos/jonsterling/tt-singletons/issues/2/events","html_url":"https://github.com/jonsterling/tt-singletons/issues/2","id":53980331,"number":2,"title":"Cleanup the monad","user":{"login":"jonsterling","id":55057,"avatar_url":"https://avatars.githubusercontent.com/u/55057?v=3","gravatar_id":"","url":"https://api.github.com/users/jonsterling","html_url":"https://github.com/jonsterling","followers_url":"https://api.github.com/users/jonsterling/followers","following_url":"https://api.github.com/users/jonsterling/following{/other_user}","gists_url":"https://api.github.com/users/jonsterling/gists{/gist_id}","starred_url":"https://api.github.com/users/jonsterling/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/jonsterling/subscriptions","organizations_url":"https://api.github.com/users/jonsterling/orgs","repos_url":"https://api.github.com/users/jonsterling/repos","events_url":"https://api.github.com/users/jonsterling/events{/privacy}","received_events_url":"https://api.github.com/users/jonsterling/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":2,"created_at":"2015-01-11T03:25:52Z","updated_at":"2015-01-11T07:56:26Z","closed_at":null,"body":"- checked/typed exceptions are anti-modular; try basing stuff off of MonadThrow or something to get that SML feel\r\n- let me run the thing in IO if I please"},"comment":{"url":"https://api.github.com/repos/jonsterling/tt-singletons/issues/comments/69486669","html_url":"https://github.com/jonsterling/tt-singletons/issues/2#issuecomment-69486669","issue_url":"https://api.github.com/repos/jonsterling/tt-singletons/issues/2","id":69486669,"user":{"login":"jonsterling","id":55057,"avatar_url":"https://avatars.githubusercontent.com/u/55057?v=3","gravatar_id":"","url":"https://api.github.com/users/jonsterling","html_url":"https://github.com/jonsterling","followers_url":"https://api.github.com/users/jonsterling/followers","following_url":"https://api.github.com/users/jonsterling/following{/other_user}","gists_url":"https://api.github.com/users/jonsterling/gists{/gist_id}","starred_url":"https://api.github.com/users/jonsterling/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/jonsterling/subscriptions","organizations_url":"https://api.github.com/users/jonsterling/orgs","repos_url":"https://api.github.com/users/jonsterling/repos","events_url":"https://api.github.com/users/jonsterling/events{/privacy}","received_events_url":"https://api.github.com/users/jonsterling/received_events","type":"User","site_admin":false},"created_at":"2015-01-11T07:56:26Z","updated_at":"2015-01-11T07:56:26Z","body":"I am still interested in them, but at this point I am not sure that constrained exceptions are even a good idea. Something like extensible sums could help, but as you say, I am not sure it's worth putting the time into just for exceptions.\r\n\r\nBy the way, slightly off topic—I've been doing some thinking about judgements, or more specifically, who it is who is doing the \"judging\" and what are they allowed to do whilst judging. Anyway, so far as I can tell, it seems like the ideal/intuitionistic judger (what Brouwer calls the creating/creative subject) has access to a wide range of effects, and the only ones I can truly consider ruling out are of two kinds:\r\n\r\n1. non-termination \r\n2. things that were at one point true becoming false (i.e. in violation of Brouwer's laws for the creative subject; this corresponds with monotonicity in a Kripke model)\r\n\r\nOther than that, it seems like it is philosophically acceptable to be pretty unconstrained wrt. effects, and so I do not really see a problem with allowing arbitrary exceptions (i.e. refuting an assertion), or even IO (i.e. consulting an oracle, which is not ruled out in intuitionism). I'm sure the more proof-theoretically inclined may take disagreement with some of this, but IMO the standard gamut of ML-style effects is a pretty ideal site for judging assertions."}}