Hacker News new | ask | show | jobs
by ben509 2925 days ago
Haskell is a proving ground, so it's picked up a number of ideas that never quite panned out.

I think you can identify a core set of features that are pretty reasonable. I think that'd be type classes, constraints, and functional dependencies.

If they made a handful of extensions standard (GADTs, etc.) it would mostly Do What You Want without a lot of prodding.

> And from Java I know that there's a pretty trivial example that showcases how its Generics implementation is unsound when mixed with inheritance.

I'd be curious to see that. There's a well known limitation that mutable containers (and they're all mutable in Java) need to be invariant, but that doesn't make them unsound.

The type system was also already unsound due to covariant arrays and nulls being a member of all classes, but if you don't break those rules or disable checks, Java generics work as far as I can tell. By "work", I mean I've yet to get a ClassCastException in a fair amount of work with some gnarly Java generics.

And, really, 99% of the boilerplate in Java's typing is that you can't declare aliases for types; that seems to be more due to engrained hostility to syntactic sugar than any technical difficulty.

> So, is there any version that just works, and never leads the user down any rabbit holes?

Most of the "gradual typing" projects for languages like Javascript, Python, Ruby all seem to accomplish what you're looking for, by virtue of the fact that you can just ignore it when you don't want it.
2 comments
jstimpfle 2925 days ago
> There's a well known limitation that mutable containers (and they're all mutable in Java) need to be invariant, but that doesn't make them unsound.

I see. Yeah I don't know precisely what these terms mean. If the creators of Generics mistakenly made them covariant, that only goes to show that maybe it's a little too complicated. IMHO.

To be more precise, what we want to do might be too complicated for practical (i.e. relatively simple) type systems to describe. So, why bother at all? Better learn how to structure programs simple enough to make them obviously correct (i.e. mistakes will be obvious and can be easily fixed). Instead of catering to the needs of impractical type systems. I think that's why C is still so popular: It removes most of the boilerplate (i.e. strides for array indexing, arithmetic operators, structs, other ABI things) but gets out of the users way if s/he needs to disregard these constraints for a while.

Even in C, there is a similar problem with const compatibility of pointers of more than 1 level of indirection. Example taken from [1]

    const int **pp2;
    int *p1;
    const int n = 13;
 
    pp2 = &p1; /* not allowed, but suppose it were */
    *pp2 = &n; /** valid, both const, but sets p1 to point at n */
    *p1 = 10;  /* valid, but changes const n */
[1] https://www.sanfoundry.com/c-tutorials-concept-pointer-compa...
link
jhomedall 2924 days ago
> I'd be curious to see that.

https://twitter.com/joshbloch/status/822948565433466881

link