search

jonsterling / tt-singletons

experiments with singleton types & identity types in type theory
MIT License
3 stars 0 forks source link

Cleanup the monad #2

Closed jonsterling closed 9 years ago

jonsterling commented 9 years ago
ghost commented 9 years ago

Are you still interested in the coproducts or corecords thing for Vinyl? Might be more work than it'd be worth just for exceptions here but it could be an interesting option…

jonsterling commented 9 years ago

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.

By 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:

  1. non-termination
  2. 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)

Other 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.

ghost commented 9 years ago

I think I agree with most of your points, fwiw. Just having extensible sums would probably not be enough although it would be nice to have in general I think. IIRC, Edward Yang posted an implementation of something like SML style exceptions in Haskell using some clever hacks. I never tried it though.

jonsterling commented 9 years ago

Yes... And you're right that extensible sums don't approximate SML style exceptions, I think they just lessen the pain of not using SML style exceptions.

I recall coming across Edward Yang's implementation a while back... I think that the aspect of SML exceptions he was getting back was their generativity (i.e. each time you open a module, you get new exceptions); I think this aspect doesn't really come up in Haskell since we don't even have modules (so it doesn't seem like I'd be able to get much advantage from that crucial aspect). The other side of exceptions is the dynamic open sum, and in the absence of modules, the nasty typeable nonsense you've got to do in Haskell works OK (especially now that you don't implement the type class yourself).

Heh, honestly I'd just rather use ML for all of this since it is well-suited—except for the fact that I could not give a signature for ABTs that ruled out malformed syntax, which seemed pretty important. (Well, maybe it is possible nowadays in OCaml, but it would likely be a bit gnarly). In all other respects, probably due to its heritage in the LCF tradition, ML is ideally suited for this kind of work.

ghost commented 9 years ago

I recall coming across Edward Yang's implementation a while back... I think that the aspect of SML exceptions he was getting back was their generativity (i.e. each time you open a module, you get new exceptions); I think this aspect doesn't really come up in Haskell since we don't even have modules (so it doesn't seem like I'd be able to get much advantage from that crucial aspect). The other side of exceptions is the dynamic open sum, and in the absence of modules, the nasty typeable nonsense you've got to do in Haskell works OK (especially now that you don't implement the type class yourself).

That sounds about right. I remember that what I saw didn't seem compelling enough in practice to bother pursuing it further.

Heh, honestly I'd just rather use ML for all of this since it is well-suited—except for the fact that I could not give a signature for ABTs that ruled out malformed syntax, which seemed pretty important. (Well, maybe it is possible nowadays in OCaml, but it would likely be a bit gnarly). In all other respects, probably due to its heritage in the LCF tradition, ML is ideally suited for this kind of work.

Yeah, I don't blame you… heh. OCaml might be doable but you'd probably have to implement a lot of basic supporting stuff.

Not really an ML replacement, but I was actually considering trying to do your ABT thing in Rust. I've implemented enough of the type-level stuff from shapeless that it might be feasible. There'd still be the lack of higher-kinded types although I think the path approach I described recently should provide a general workaround (if somewhat tedious). No exceptions either but you can at least do the same sort of typeable thing. Probably gnarly though… :]

jonsterling commented 9 years ago

ABTs in Rust would be pretty interesting!