On Sat, Apr 4, 2015 at 7:05 AM, Keean Schupke <[email protected]> wrote: > On 4 April 2015 at 11:44, Matt Oliveri <[email protected]> wrote: >> >> You are missing the point. Type-level expressions may not denote >> types, but the point of type-level expressions is they will be used as >> subexpressions for type expressions. In order to ensure that type >> inference algorithms do not encounter cases they can't handle, we >> generally need to restrict types on the basis of the non-type >> subexpressions they can use. > > I don't think this needs to be a problem for inference, I think you can > design inference so that it does work, but you sometimes have to take the > right design decisions. For example in Mark Jones's FCP you can infer types > for higher order expressions, but you can't do this in Haskell, and it > requires type-annotations.
You are _still_ missing the point. The need to make the right design decisions is exactly what I'm talking about. I'm only pointing out that part of that decision is what to allow in non-type, type-level expressions. Unless you're claiming that allowing arbitrary type-level computations would still not break unification (for example). But I don't think you're saying that, 'cause it seems pretty clear that it would, and I don't know much of anything about fancy type inference. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
