4 ms·
Type error. your lambda doesn't have a valid static type signature. You would wrap that around a union type: wtf = A of string | B of float And then you'd ret
by jldugger 6y ago
Type error. your lambda doesn't have a valid static type signature. You would wrap that around a union type:
wtf = A of string | B of float
And then you'd return A("abc") or B(2.01) and your function would be () -> wtf
- chrisseaton 6y agoWhy's it a type error rather than inferring a sum type?
- iaabtpbtpnn 6y agoYou can get it to infer the sum type by giving tags to your values with backticks, like `A 1.23 and `B "foo". This will be inferred as "`A of int | `B of string" without you having to declare any type. Without those tags, the system assumes you have made a mistake in returning values of separate types. If it didn't do that, you would not get type errors in many/most (all?) of the situations where you want the type system to help by indicating the inconsistency to you.
- chrisseaton 6y agoGiving tags seems like declaring a type though?
- lmm 6y agoIt's not though. If we think about Result as an example, `1`, `Success(1)` and `Failure(1)` are different values, not just different types. I think the point you're making is that Standard ML has certain restrictions in its type system that are necessary to make type inference possible: there are no union types, no subtypes (more recent work has found a way to make subtyping compatible with full H-M), polymorphism has to be introduced explicitly with `let`, and there are no higher-kinded types. And in some cases you'd argue those restrictions might incur more code overhead compared to a language that loosens those restrictions at the cost of less reliable type inference (e.g. Scala). That's sort-of-but-not-really true: in my experience union types and subtypes are always bad ideas and there are better alternatives for any use case where you would use them. You never actually want "String | Int", you want a type with meaningful semantics (like `Result<String, Int>`).
- 3001 6y agoDon't take my word for it but I don't think you can implicitly unify[0] two base type in HM. https://www.cs.cornell.edu/courses/cs3110/2011sp/Lectures/lec26-type-inference/type-inference.htm https://www.cs.cornell.edu/courses/cs3110/2011sp/Lectures/le...
- shpongled 6y agoYou cannot unify a string and an integer. 'Base type' is just an abstraction over the enumerable primitive types (bool, unit, char, etc). It's generally understood that these are simple cases to unify, so they aren't even mentioned most of the time.
- nulptr 6y agobecause "ssdf" is a string but B("asd") is user-defined sum type. So in the original example, you can't unify "ssdf" and the int 33, but in the re-written version B("sfd") and A(33) have the same type and can be unified.
- ufo 6y agoIf you use the "polymorphic variants" feature with backticks it automatically infers the union. However, most of the time the regular non-polymorphic variants are easier to work with. A good discussion of this can be found in https://dev.realworldocaml.org/variants.html#scrollNav-4 https://dev.realworldocaml.org/variants.html#scrollNav-4
- ralfn 6y agoYou might like the language Crystal, it works this way. https://crystal-lang.org/ https://crystal-lang.org/
- chrisseaton 6y agoBut Crystal recently had to walk back from global type inference as they found it was not realistic in practice, didn't they?
- gnulinux 6y agoWhy is it not realistic? Is it too slow or too unreadable?
- chrisseaton 6y agoYou could dig up the mailing list messages at the time, but yeah it was slow and I think it produced error messages that were extremely hard to use - it would decide the type of functions was something nonsensical and then report that as an error at all the call sites instead.
- gnulinux 6y agoMakes sense, bad errors is also why I don't use type inference in my code.
- dependenttypes 6y agoIf you are interested for a language that does something like that then check out https://archive.is/Op8Mf https://archive.is/Op8Mf or the other words by Stephen Dolan