4 ms·

Can't a compiler be created to traverse the AST, locate all operations performed on the variable and infer the narrowest type definition that allows for all of

by hliyan 9y ago

Can't a compiler be created to traverse the AST, locate all operations performed on the variable and infer the narrowest type definition that allows for all of those operations, and then enforce at compile time? Edit: example to further clarify what I meant (it's a bit more than type inference at initial assignment) var x = readUserInput(); // narrow down: string, int, double x += y; // if y is also a user input, no change x += 1; // narrow down to int, double p = x % 2; // narrow down to int

llimllib 9y ago
My understanding is that Julia does something like this? But I'm far from an expert.
- dnautics 9y ago
  Yep. Julia is a great language and I think other languages could learn from it, especially it's typing model and the excellent implementation of the REPL. but I wouldn't say Julia is good for everything (I wouldn't want to write a web service in it).
bastawhiz 9y ago
Many languages do this (type inference), to some extent. The moment you have any expression that can evaluate to more than one type, though, it requires annotations.
- hliyan 9y ago
  Are there any languages that do it beyond the first value assignment, or outside the current scope? Also, any languages that subsequently revise the type definition?
  - tedmiston 9y ago
    Not sure if this is exactly what you're asking but one can reassign variables to change their types in Python: >>> x = 1 >>> type(x) <class 'int'> >>> x = 'foo' >>> type(x) <class 'str'>
    - xapata 9y ago
      I believe the question was about inferred static typing for union types. Python does not do any static type inference. Also, I'm not sure how a union type could be distinguished from an error during type inference. Maybe a nullable, but otherwise it'd be very tricky.
- bitwalker 9y ago
  That's not always true, rank-1 polymorphic functions (i.e. functions polymorphic in their argument) don't usually require type annotations. Higher-rank polymorphic functions though do generally require them, because without the annotations type inference is undecidable in the general case for such functions. For example: pair x y = (x, y) This function creates a pair for any two types, and doesn't require any annotations.
kreetx 9y ago
Depending on how versed you are in typed languages, but it looks like you're describing type inference, which exists in Haskell and in some other languages as well. I.e you don't need to add type signatures everywhere. But gradual typing means avoiding typing alltogether in some parts of the program and in some sense going against the inferred type. This is probably most relevant in Haskell where IO is typed, and less so in others, e.g Clojure.
- hliyan 9y ago
  I come from a C++ background, with a recent interest in JavaScript and Go. I'm trying to envision something a little more than simple inference. I'm imagining how I would take an untyped codebase and how I will infer the data type of a variable or a parameter by studying all its usages within the code.
  - wtetzner 9y ago
    It depends on the type system, but often all usages are taken into account during type inference.
  - ufo 9y ago
    That would still fall under the umbrella of "type inference" If you want to learn more about this, the Damas Milner unification-based algorithm used in ML, Haskell and others is a must-read starting point. It does global type inference of all types in the program without requiring any annotations, by analyzing how the types are used. It also can detect when a variable is only passed around, without being used in primitive operations, in which case it infers a generic/parametric type for it.
  - int_19h 9y ago
    Coming from C++, take a look at OCaml, and specifically it's object-oriented facilities. It does exactly what you want, but in an usual (for a C++ coder) way - by making objects structurally typed. Suppose you write a function like this: let f(x, y) = x#foo(y#bar(x)) `#` is the member access operator. So this is a function that takes two objects (strictly speaking, it takes a single tuple of two objects), calls the method `bar` on `y` passing `x` as argument, then calls the method `foo` on `x` passing the result of the previous call as argument, and finally returns the result of that. Nowhere are the types declared, but they are fully inferred and statically checked. The actual type of `f` is rather convoluted when written out fully: (<foo: 'b -> 'c; ..> as 'a) * (<bar: 'a -> 'b; ..>) -> 'c The `<>` notation means "object", with members listed inside delimited by semicolons. `foo: 'b -> 'c` means that there must be a member named "foo", which is a function that takes a single argument of some type 'b, and returns a value of some other type 'c - these are like template type parameters in C++, except you don't have to declare them. Finally, `..` means "and any other members" - without it, our function would only accept objects that have only the member named "foo" with the designated signature. So, `<foo: 'b -> 'c; ..>` means "any object that has method "foo" that takes a value and returns a value, and also possibly some other members". The `as 'a` part then assigns another type parameter to describe that object for reference later. Then we see the object type for the second function argument, which is `<bar: 'a -> 'b; ..>`. This is structured in the same way, but note that it uses type parameters with the same names as before - this indicates that they must be the same type. This makes it possible to make the definitions recursive; the entire bit before `-> 'c` at the end can be described in a more verbose fashion like so: "A tuple, the first element of which is an object, with method "foo", taking an argument of the same type that is returned by method "bar" of the second element of the tuple, and returning a value of any type, and possibly some other members; and the second element of which is an object, with method "bar", taking an argument of the same type as the first element, and returning a value of the same type that method "foo" takes as an argument, and possibly some other members." Note that you don't actually need to write any of this. You can explicitly declare the type of "f" if you want to, but the compiler can figure it all out by itself, just by looking at the body, and will print out the type for you. It will also statically verify how the function is used. So, this is okay: let a_foo = object method foo y = y + 1 end;; let a_bar = object method bar x = x#foo 0 end;; f(a_foo, a_bar) But on the other hand, this: f(a_bar, a_foo) gives a compile-time error for the first argument: This expression has type < bar : < foo : int -> 'a; .. > -> 'a > but an expression was expected of type < foo : 'b -> 'c; .. > The first object type has no method foo And this: f(a_foo, a_foo) gives an error for the second: This expression has type < foo : int -> int > but an expression was expected of type < bar : < foo : int -> int > -> int; .. > The first object type has no method bar (OCaml also has classes, but their sole purpose is to provide a common implementation for objects, and to allow code reuse and extensibility via inheritance; classes aren't types, and class inheritance does not necessarily denote subtyping.) Effectively, this is static duck typing. This all looks a great deal like C++ templates, in that you can "just do" things, and the validity is effectively determined at the point of use. However, because it is captured at the type system level, the point of use doesn't have to see the implementation of your "template" to typecheck it - it just checks the arguments against the type signature that it computed when the "template" was defined. This also means that `f` is an actual function - not really a template - and so it can be passed around, stored in a variable etc (which in C++ is only possible for specific instantiations of a template).
pizza234 9y ago
You're describing type inference. An example is Crystal; [edited] example from the website: if rand(2) > 0 my_string = "hello world" end puts my_string.upcase Execution: $ crystal hello_world.cr Error in hello_world.cr:4: undefined method 'upcase' for Nil (compile-time type is (String | Nil))
- hliyan 9y ago
  I edited my comment to explain further -- I'm talking about going beyond the initial assignment...
  - nytopop 9y ago
    Check out the hindley milner type system [1]. It's used by haskell and some other languages, and allows for a very extensive amount of type inference. You can often write large sections of code with no type annotations and the compiler can figure out the most general type based on the type of some function called somewhere, which means the thing you did with that result must be of a certain class of types, which makes the surrounding expressions' types have to be a certain class of types, etc etc. [1] https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_sy...
    - cwzwarich 9y ago
      I think it's fair to say that (GHC) Haskell no longer really uses the Hindley-Milner type system. It doesn't have let generalization (except in a few restricted cases), and it doesn't have principal types, which I would consider to be the two distinguishing features of HM.
      - danharaj 9y ago
        Let generalization should only be disabled if one uses the GADT type extension and even then can be turned on in addition to GADTs. While Haskell isn't really Hindley-Milner, it's close enough for most development.
emodendroket 9y ago
What do you do about two types with methods that have the same signature?
- hliyan 9y ago
  It will need to be a language without method overloading.
  - emodendroket 9y ago
    So no two classes anywhere in the entire project can have a method with the same signature?
    - gizmo686 9y ago
      No, they just cant have the same name if they are in the same namespace. Even languages with overloading dont allow them in the same namespace if they also have the same signature.
      - emodendroket 9y ago
        How does this hypothetical compiler know whether to take NamespaceA.Queue.Size or NamespaceB.DynamicArray.Size or NamespaceC.File.Size?
        gizmo686 9y ago
        Because a compiler will only load symbols from the current namespace. If you import both Queue.Size and DynamicArray.Size, then try to call Size, the compiler may fail due to the ambiguous reference to "Size". If you wanted access to both of them in the same namespace, you would have to do some form of a qualified import/reference to disambiguate for the compiler. This is the way that any language that does not support overloading handles this, regardless of type system. It is also possible for the compiler to use type information to attempt to disambiguate. Especially because this would normally happen across module boundaries, a hypothetical compiler could: 1) Infer types based on all non-ambiguous references (or all references within the compilation unit that contains the definition) 2) Disambiguate all ambiguous reference using type information. I suppose a sufficiently smart compiler could attempt to do type inference and disambiguation at the same time; but that sounds like introducing NP hard problems to the compiler for the sole purpose of allowing confusing code.
seanmcdirmid 9y ago
Yes. It works well as long as you have all the pieces and don’t have to worry about nominal subtypes.
- hliyan 9y ago
  Could you explain a little more about the complications of nominal subtypes?
  - seanmcdirmid 9y ago
    I should have qualified that with the presence of type parameters (nominal subtypes without type parameters are still easy to deal with). Without subtypes, you only unify X and Y (so X = Y), where X and Y are trees with open variables. It turns out X < Y is much harder (semi unification rather than unification). It is basically equivalent to an alias analysis with imperative assignments (subtypes) and fields (type parameters).
    - chillee 9y ago
      You might have seen this already, but there was a thesis on combining subtyping and type inference here: http://www.cl.cam.ac.uk/~sd601/papers/mlsub-preprint.pdf http://www.cl.cam.ac.uk/~sd601/papers/mlsub-preprint.pdf
      - seanmcdirmid 9y ago
        It’s an active research area (less so now than in the 90s), so there is a lot of work on the subject. Nothing in production beyond ordersky’s color type system in scale (and that is completely local). Also, I believe the work you are citing above explores structural subtypes, not nominal ones.
shados 9y ago
Call site analysis and such are ways to do that. That's for example the difference between TypeScript and Flow. The later does stuff like that (which is both a boon and a bane. Its amazingly powerful, but you can get into states where figuring out why you're getting a compile time error is a mind fuck. Languages Elm handle it beautifully though.
SolarNet 9y ago
Julia does exactly this.

by hliyan 9y ago

llimllib 9y ago

My understanding is that Julia does something like this? But I'm far from an expert.

dnautics 9y ago
Yep. Julia is a great language and I think other languages could learn from it, especially it's typing model and the excellent implementation of the REPL. but I wouldn't say Julia is good for everything (I wouldn't want to write a web service in it).

bastawhiz 9y ago

Many languages do this (type inference), to some extent. The moment you have any expression that can evaluate to more than one type, though, it requires annotations.

hliyan 9y ago
Are there any languages that do it beyond the first value assignment, or outside the current scope? Also, any languages that subsequently revise the type definition?
- tedmiston 9y ago
  Not sure if this is exactly what you're asking but one can reassign variables to change their types in Python: >>> x = 1 >>> type(x) <class 'int'> >>> x = 'foo' >>> type(x) <class 'str'>
  - xapata 9y ago
    I believe the question was about inferred static typing for union types. Python does not do any static type inference. Also, I'm not sure how a union type could be distinguished from an error during type inference. Maybe a nullable, but otherwise it'd be very tricky.
bitwalker 9y ago
That's not always true, rank-1 polymorphic functions (i.e. functions polymorphic in their argument) don't usually require type annotations. Higher-rank polymorphic functions though do generally require them, because without the annotations type inference is undecidable in the general case for such functions. For example: pair x y = (x, y) This function creates a pair for any two types, and doesn't require any annotations.

kreetx 9y ago

Depending on how versed you are in typed languages, but it looks like you're describing type inference, which exists in Haskell and in some other languages as well. I.e you don't need to add type signatures everywhere. But gradual typing means avoiding typing alltogether in some parts of the program and in some sense going against the inferred type. This is probably most relevant in Haskell where IO is typed, and less so in others, e.g Clojure.

hliyan 9y ago
I come from a C++ background, with a recent interest in JavaScript and Go. I'm trying to envision something a little more than simple inference. I'm imagining how I would take an untyped codebase and how I will infer the data type of a variable or a parameter by studying all its usages within the code.
- wtetzner 9y ago
  It depends on the type system, but often all usages are taken into account during type inference.
- ufo 9y ago
  That would still fall under the umbrella of "type inference" If you want to learn more about this, the Damas Milner unification-based algorithm used in ML, Haskell and others is a must-read starting point. It does global type inference of all types in the program without requiring any annotations, by analyzing how the types are used. It also can detect when a variable is only passed around, without being used in primitive operations, in which case it infers a generic/parametric type for it.
- int_19h 9y ago
  Coming from C++, take a look at OCaml, and specifically it's object-oriented facilities. It does exactly what you want, but in an usual (for a C++ coder) way - by making objects structurally typed. Suppose you write a function like this: let f(x, y) = x#foo(y#bar(x)) `#` is the member access operator. So this is a function that takes two objects (strictly speaking, it takes a single tuple of two objects), calls the method `bar` on `y` passing `x` as argument, then calls the method `foo` on `x` passing the result of the previous call as argument, and finally returns the result of that. Nowhere are the types declared, but they are fully inferred and statically checked. The actual type of `f` is rather convoluted when written out fully: (<foo: 'b -> 'c; ..> as 'a) * (<bar: 'a -> 'b; ..>) -> 'c The `<>` notation means "object", with members listed inside delimited by semicolons. `foo: 'b -> 'c` means that there must be a member named "foo", which is a function that takes a single argument of some type 'b, and returns a value of some other type 'c - these are like template type parameters in C++, except you don't have to declare them. Finally, `..` means "and any other members" - without it, our function would only accept objects that have only the member named "foo" with the designated signature. So, `<foo: 'b -> 'c; ..>` means "any object that has method "foo" that takes a value and returns a value, and also possibly some other members". The `as 'a` part then assigns another type parameter to describe that object for reference later. Then we see the object type for the second function argument, which is `<bar: 'a -> 'b; ..>`. This is structured in the same way, but note that it uses type parameters with the same names as before - this indicates that they must be the same type. This makes it possible to make the definitions recursive; the entire bit before `-> 'c` at the end can be described in a more verbose fashion like so: "A tuple, the first element of which is an object, with method "foo", taking an argument of the same type that is returned by method "bar" of the second element of the tuple, and returning a value of any type, and possibly some other members; and the second element of which is an object, with method "bar", taking an argument of the same type as the first element, and returning a value of the same type that method "foo" takes as an argument, and possibly some other members." Note that you don't actually need to write any of this. You can explicitly declare the type of "f" if you want to, but the compiler can figure it all out by itself, just by looking at the body, and will print out the type for you. It will also statically verify how the function is used. So, this is okay: let a_foo = object method foo y = y + 1 end;; let a_bar = object method bar x = x#foo 0 end;; f(a_foo, a_bar) But on the other hand, this: f(a_bar, a_foo) gives a compile-time error for the first argument: This expression has type < bar : < foo : int -> 'a; .. > -> 'a > but an expression was expected of type < foo : 'b -> 'c; .. > The first object type has no method foo And this: f(a_foo, a_foo) gives an error for the second: This expression has type < foo : int -> int > but an expression was expected of type < bar : < foo : int -> int > -> int; .. > The first object type has no method bar (OCaml also has classes, but their sole purpose is to provide a common implementation for objects, and to allow code reuse and extensibility via inheritance; classes aren't types, and class inheritance does not necessarily denote subtyping.) Effectively, this is static duck typing. This all looks a great deal like C++ templates, in that you can "just do" things, and the validity is effectively determined at the point of use. However, because it is captured at the type system level, the point of use doesn't have to see the implementation of your "template" to typecheck it - it just checks the arguments against the type signature that it computed when the "template" was defined. This also means that `f` is an actual function - not really a template - and so it can be passed around, stored in a variable etc (which in C++ is only possible for specific instantiations of a template).

pizza234 9y ago

You're describing type inference. An example is Crystal; [edited] example from the website: if rand(2) > 0 my_string = "hello world" end puts my_string.upcase Execution: $ crystal hello_world.cr Error in hello_world.cr:4: undefined method 'upcase' for Nil (compile-time type is (String | Nil))

hliyan 9y ago
I edited my comment to explain further -- I'm talking about going beyond the initial assignment...
- nytopop 9y ago
  Check out the hindley milner type system [1]. It's used by haskell and some other languages, and allows for a very extensive amount of type inference. You can often write large sections of code with no type annotations and the compiler can figure out the most general type based on the type of some function called somewhere, which means the thing you did with that result must be of a certain class of types, which makes the surrounding expressions' types have to be a certain class of types, etc etc. [1] https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_sy...
  - cwzwarich 9y ago
    I think it's fair to say that (GHC) Haskell no longer really uses the Hindley-Milner type system. It doesn't have let generalization (except in a few restricted cases), and it doesn't have principal types, which I would consider to be the two distinguishing features of HM.
    - danharaj 9y ago
      Let generalization should only be disabled if one uses the GADT type extension and even then can be turned on in addition to GADTs. While Haskell isn't really Hindley-Milner, it's close enough for most development.

emodendroket 9y ago

What do you do about two types with methods that have the same signature?

hliyan 9y ago
It will need to be a language without method overloading.
- emodendroket 9y ago
  So no two classes anywhere in the entire project can have a method with the same signature?
  - gizmo686 9y ago
    No, they just cant have the same name if they are in the same namespace. Even languages with overloading dont allow them in the same namespace if they also have the same signature.
    - emodendroket 9y ago
      How does this hypothetical compiler know whether to take NamespaceA.Queue.Size or NamespaceB.DynamicArray.Size or NamespaceC.File.Size?
      - gizmo686 9y ago
        Because a compiler will only load symbols from the current namespace. If you import both Queue.Size and DynamicArray.Size, then try to call Size, the compiler may fail due to the ambiguous reference to "Size". If you wanted access to both of them in the same namespace, you would have to do some form of a qualified import/reference to disambiguate for the compiler. This is the way that any language that does not support overloading handles this, regardless of type system. It is also possible for the compiler to use type information to attempt to disambiguate. Especially because this would normally happen across module boundaries, a hypothetical compiler could: 1) Infer types based on all non-ambiguous references (or all references within the compilation unit that contains the definition) 2) Disambiguate all ambiguous reference using type information. I suppose a sufficiently smart compiler could attempt to do type inference and disambiguation at the same time; but that sounds like introducing NP hard problems to the compiler for the sole purpose of allowing confusing code.

seanmcdirmid 9y ago

Yes. It works well as long as you have all the pieces and don’t have to worry about nominal subtypes.

hliyan 9y ago
Could you explain a little more about the complications of nominal subtypes?
- seanmcdirmid 9y ago
  I should have qualified that with the presence of type parameters (nominal subtypes without type parameters are still easy to deal with). Without subtypes, you only unify X and Y (so X = Y), where X and Y are trees with open variables. It turns out X < Y is much harder (semi unification rather than unification). It is basically equivalent to an alias analysis with imperative assignments (subtypes) and fields (type parameters).
  - chillee 9y ago
    You might have seen this already, but there was a thesis on combining subtyping and type inference here: http://www.cl.cam.ac.uk/~sd601/papers/mlsub-preprint.pdf http://www.cl.cam.ac.uk/~sd601/papers/mlsub-preprint.pdf
    - seanmcdirmid 9y ago
      It’s an active research area (less so now than in the 90s), so there is a lot of work on the subject. Nothing in production beyond ordersky’s color type system in scale (and that is completely local). Also, I believe the work you are citing above explores structural subtypes, not nominal ones.

shados 9y ago

Call site analysis and such are ways to do that. That's for example the difference between TypeScript and Flow. The later does stuff like that (which is both a boon and a bane. Its amazingly powerful, but you can get into states where figuring out why you're getting a compile time error is a mind fuck. Languages Elm handle it beautifully though.

SolarNet 9y ago

Julia does exactly this.