4

Suppose we have a functional language where objects don't have explicitly defined types, but where named properties can nonetheless be accessed on objects. Is it then possible for the compiler to trace throughout the program which properties could be accessed on which variables and do full type inference on the program so that if the program compiles, it's guaranteed that all accessed properties must exist? For example, each property name could correspond to a Haskell typeclass and the compiler could check the soundness using Hindley-Milner.

Note that like with most compilers, the compiler would be checking types on variables, not objects. Therefore it would reject some programs all of whose property accesses are valid. Accepting a program if and only if all its accesses are valid is obviously uncomputable, and that is not what I am suggesting the compiler do.

Does this method of type checking work? Would it be practical? If so, why is it not used as a compromise between dynamically and statically typed languages?

  • 2
    Once you have modules the "trace throughout the program" idea becomes a little dicey. Also, doing that is likely to be costly and perhaps confusing once you need to trace down the root cause of an access. – Telastyn May 8 '17 at 22:08
  • 1
    Seems like a question that Computer Science might like. – Josh Caswell May 8 '17 at 22:20
  • 1
    Have a look at Go Language's implied interfaces. It's similar to what you're describing, though I think it approaches it from the opposite direction. Implied interfaces are a form of duck typing. – Robert Harvey May 8 '17 at 22:41
  • 3
    Why do you want to "infer types" in language without "explicitly defined types"? – el.pescado May 10 '17 at 6:04
  • 1
    What happens if members on two objects with the same name have two different types? What about overloads? I would suppose it would be possible, but it might be a bit hairy. How would writing methods work, before they're being used? You'd have no intellisense, and none of it would compile until it had at least one caller. It seems backwards to the idea of designing completely encapsulated logic. Instead of you telling others how to use your API, others tell you how they're using the API. – Rob May 10 '17 at 6:27
2

Suppose we have a functional language where objects don't have explicitly defined types, but where named properties can nonetheless be accessed on objects. Is it then possible for the compiler to trace throughout the program which properties could be accessed on which variables and do full type inference on the program so that if the program compiles, it's guaranteed that all accessed properties must exist? For example, each property name could correspond to a Haskell typeclass and the compiler could check the soundness using Hindley-Milner.

Yeah, we can do something a lot like that! But I doubt that it would be practical.

Let's take a look at what this might look like. Consider the following ordinary Python function (taken from https://github.com/fchollet/keras/blob/master/tests/keras/test_sequential_model.py):

def test_sequential_pop():
    model = Sequential()
    model.add(Dense(num_hidden, input_dim=input_dim))
    model.add(Dense(num_class))
    model.compile(loss='mse', optimizer='sgd')
    x = np.random.random((batch_size, input_dim))
    y = np.random.random((batch_size, num_class))
    model.fit(x, y, epochs=1)
    model.pop()
    assert len(model.layers) == 1
    assert model.output_shape == (None, num_hidden)
    model.compile(loss='mse', optimizer='sgd')
    y = np.random.random((batch_size, num_hidden))
    model.fit(x, y, epochs=1)

Suppose we want to do duck typing, and we want type inference as well. Python doesn't have type inference, of course, but Haskell does, and we can convince Haskell to do something a lot like duck typing.

Duck typing means that we don't really care about the actual types of all the things we're using; all we care about is that the things can be used together, in the way we're using them. In order to make Haskell happy with that, we'll use implicit parameters in order to create objects and access their properties. Just like we want, the compiler will trace what properties are being accessed on which variables, and so forth.

Our Haskell code might look like this:

testSequentialPop = do
    model <- ?newSequential
    ?newDense numHidden (Just inputDim) >>= ?addLayer model
    ?newDense numClass Nothing >>= ?addLayer model
    ?compileModel model "mse" "sgd"
    x <- ?getRandom [batchSize, inputDim]
    y <- ?getRandom [batchSize, numClass]
    ?fitModel model x y 1
    ?popModel model
    ?assert (?length (?layers model) == 1)
    ?assert (?outputShape model == [Nothing, Just numHidden])
    ?compileModel model "mse" "sgd"
    y2 <- ?getRandom [batchSize, numHidden]
    ?fitModel model x y 1

So far, so good. This code will compile just fine. If we write the rest of the program, it will run just fine, too.

So what's the problem? Let's ask GHC what the type of testSequentialPop is. GHC says:

testSequentialPop
  :: (Eq a5, Eq a7, Monad m, Num a2, Num a3, Num a5, Num a7, Num t2,
      Num a9, ?addLayer::t -> a1 -> m a, ?assert::Bool -> m a6,
      ?compileModel::t -> [Char] -> [Char] -> m a8,
      ?fitModel::t -> t1 -> t1 -> a9 -> m b, ?getRandom::[t2] -> m t1,
      ?layers::t -> t3, ?length::t3 -> a5,
      ?newDense::a2 -> Maybe a3 -> m a1, ?newSequential::m t,
      ?outputShape::t -> [Maybe a7], ?popModel::t -> m a4) =>
     m b

Ooh, that's pretty complicated.

The problem here is that the function has to mention every operation it ever performs on the input objects. If you had a large program that does complicated things with input objects, you could end up with a type which contains hundreds, maybe thousands of constraints.

Type inference will help things a little bit, but not that much. Type inference sometimes saves programmers from having to calculate types themselves, or from having to type them out in full. Programmers will still have to understand types in order to figure out how functions can be used, and to diagnose what's causing type errors.


That said, there are tools which do something similar to this. For example, Checkmarx makes a static code analysis tool which can detect certain security vulnerabilities, such as SQL injection attacks, by tracing how objects are created and used. A SQL injection attack is essentially a duck typing error: you're creating an object (a string containing user input), and then performing an operation (using it as a SQL query) on it, even though that object does not support that operation. Checkmarx traces the entire path of this object, from creation to use, and, if it finds any problems, it shows you the entire path.

I don't know if it would be feasible to extend this idea so that it works on all operations, rather than just operations that are a security hazard.

  • Right, that's what I was thinking. Yes the types get out of hand. – Solomonoff's Secret May 11 '17 at 21:37
4

Scala does provide both type inference and structural typing (which is for all intents and purposes the same as duck typing).

In contrast to Haskell, in Scala, the type must be annotated in the function's argument (although it's option for the return type), so it's always clear what does your function requires.

This has the drawback, that if you use it it a lot, especially on big structures, your code will have a lot of redundant annotation.

EDIT:

Structural types can be named, to remove redundancy, although they rarely are:

type Duck = {def quack():String}

I personally don't think that structural types are useful in any way in Scala. Not naming your data structure does nothing good.

You can just declare a trait, so you have a named a structure and extend its behaviour via type classes. If you want to omit naming in the name of being terse, you can use tuples or HLists.

form the Scala glossary:

structural type

A refinement type where the refinements are for members not in the base type. For example, { def close(): Unit } is a structural type, because the base type is AnyRef, and AnyRef does not have a member named close.

  • One use of structural typing is as a way of bypassing most of the boilerplate associated with reflection. I do agree that for arguments it's mostly useless. – Morgen May 10 '17 at 13:59
  • 1
    I would not say structural typing is the same as duck typing. Type checking at compile time is the big advantage of structural typing over duck typing. – Frank Hileman May 11 '17 at 0:56
  • 1
    @FrankHileman There are some differences, but it's blurry, i don't think Wikipedia's definition is accurate, since it says It requires that type checking be deferred to runtime, and is implemented by means of dynamic typing or reflection. which, to me seems weird, since that's just what the most common implementations does. This stack overflow answer makes the difference much clearer, and according to that, what Scala has, is actually Duck typing, since you don't need to supply the same structure, your type just needs to have does fields. – Máté Magyar May 11 '17 at 5:14
  • @Morgen I have not seen it used instead of reflections (although i can imagine the case) but i think it's a very bad code smell if you have to do that. Type classes are much better solution for those cases. – Máté Magyar May 11 '17 at 5:25
  • Oh, I agree that's nearly always the case, especially in method parameters. When you do have to reach for reflection, there's little use in making it harder than it needs to be. The key is structural typing isn't limited to parameters, there's a few good examples here: daily-scala.blogspot.com/2010/02/… - not the first tool to reach for, but also better than dealing with the reflection API. – Morgen May 11 '17 at 5:32
1

I think this is possible as long the types themselves can't be modified at run-time, meaning you can do this

void PrintDuck(d) {
    print("The "+d.feet+" footed duck says "+d.Quack());
}

var duck = {
    int feet = 2;
    string Quack(){
        return "Quack!";
    }
}

PrintDuck(duck);

but not this

void PrintDuck(d) {
    print("The "+d.feet+" footed duck says "+d.Quack());
}

var duck = {
    string Quack(){
        return "Quack!";
    }
}

duck.feet = 2; // illegal, modifies type

PrintDuck(duck);

It's just structural typing and generics. I don't personally know of any languages that have both, but there's certainly no reason a language couldn't, and there's no reason it can't all happen at compile-time.

If you're suggesting the second example then no, it's not possible to check at compile-time. The compiler simply can't reason about fields or methods added at run-time.

0

Is it then possible for the compiler to trace throughout the program which properties could be accessed on which variables and do full type inference on the program so that if the program compiles, it's guaranteed that all accessed properties must exist?

No, I don't think so.

Objects come to life at run time, not at compile time. The compiler has no way of knowing which object will have what properties at run time.

From the Wikipedia article on Duck typing:

It requires that type checking be deferred to runtime, and is implemented by means of dynamic typing or reflection.

  • 1
    You are right that it is impossible for a compiler to allow a program if and only if all accessed properties exist, but only if is much easier. For example, the Java compiler achieves only if. It does so by rejecting some programs that would be valid by reasoning at the variable level and not the value level. – Solomonoff's Secret May 8 '17 at 21:37
  • @Solomonoff'sSecret, I am not familiar with Java. Can't comment on that. I'll let those that are familiar with Java to respond to that. – R Sahu May 8 '17 at 21:40
  • @RSahu All languages with static typing do it, if you don't use casting. Java was an example of a language with static typing. – immibis May 10 '17 at 3:38
  • 1
    @RSahu You are saying that it's completely impossible to do something that static languages already do. Static languages are irrelevant to the OP but are relevant to why this answer is incorrect. – immibis May 10 '17 at 4:45
  • 1
    The question asks about "type inference with duck typing" - i.e. code that looks like duck typing but where the compiler assigns types under the hood to allow better checking. The key definition of duck typing (from the same Wikipedia page) is "In duck typing, an object's suitability is determined by the presence of certain methods and properties (with appropriate meaning), rather than the actual type of the object." and that says nothing about how it is implemented. – immibis May 10 '17 at 7:12
-1

Your question is ill-founded - you state that no such language exists, but they clearly do; take any language with complete type inference.

  • 1
    Like what? I'm not aware of any language that does this. Certainly no mainstream language does. – Solomonoff's Secret May 10 '17 at 2:27
  • @Solomonoff'sSecret You don't know any language with complete type inference? SML, OCaml, Haskell -- I mean, Hindley-Milner is the prototypical example, which you yourself even mentioned. Unless I completely misunderstood your question. – gardenhead May 10 '17 at 2:28
  • 2
    None of these languages do what I suggest. They require you to define data types with fields before you access the fields. – Solomonoff's Secret May 10 '17 at 2:39
  • @Solomonoff's To my surprise, I double-checked and OCaml does not allow this, like you say. It must be a quirk of their type-inference algorithm. I just assumed it did because it's based on SML, which does support complete type inference (and is the language I'm most familiar with). This is also a feature of Hindley-Milner. So there are a few, and there is no reason why more languages couldn't do so. – gardenhead May 10 '17 at 3:03
  • How about Sun's "Self" language; Java's older sibling? – Evan Langlois Apr 8 '18 at 3:25

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.