bosatsu
bosatsu copied to clipboard
johnynek
WIP: extend paper to support higher rank type parameters on data constructors
related to #267 #269
In this comment: https://github.com/johnynek/bosatsu/pull/269#issuecomment-497995921
While rereading the paper I am using, they state this limitation, though I had forgotten: type constructors are all monotyped in this typesystem.
So, the kind of code that we are trying to write in #267 and #269 isn't supported. The main issue is that we always use inference on type constructor parameters, and inference always infers monotypes.
An idea I had to extend the algorithm to support this is to look to see if there are any annotations of polytypes in a data constructor, and if there, in some limited cases, we could infer a polytype (namely, if the constructor is tuple-like and has a free type parameter in one position).
This may cause other problems and it doesn't quite work, but I'm putting it up here as a sketch of an idea.
I was just coming here to ponder if this wasn't a bug and was as the type system intended. It seems the intention is that a type variable cannot subsume a quantified type (anything other than a Tau). Certainly not inferred to be.
Well, we can infer quantified types, but only certain kinds. It happens by instantiation and quantification.
I don’t really grok the predicative condition. It seems what we want is called impredecative inference, but they also say it is known that is not decidable in the presence of rank-n types.
I actually don’t care about inferring everything, but I do want to find a way to address the common cases at least with annotations.
It feels like we could solve “tuple-like” cases, which includes wrapper types like.
Also, obviously I need to understand it more clearly and give better error messages than subsumption failure. It is more that it inferred an illegal type which isn’t supported. It would be good to be able to get out of that with annotations, it seems in the case of data constructors that’s not possible.
@snoble slowly, I'm going to wind up becoming a logician here: https://www.iep.utm.edu/predicat/
I do feel a bit like someone trying to set up a quantum mechanics experiment without having taken any physics....
It may or may not surprise you to learn I took exactly 1 CS class at university (okay, well, I think a second one in grad school on cryptography)...
That is some good old fashioned early 20th century logic going on there.
What I meant by my comment is that we seem to be always failing when running subsCheck on whether a meta type subsumes something that contains a forall. And the meta came from instantiating a quantified type.
But I might have things backwards
this is related to #650 -- which is principled, unlike this PR (which may still have some useful ideas for pattern matching).