beyond myself

0%

PL(4)Part-A-Week5

发表于 更新于 分类于 ，

Ideas of Week5

Type Inference

SML has a static type system, i.e., it determines all the types for its bindings before ever executing the program. But unlike most statically typed programming languages, like C, Java, SML is implicitly typed. We don’t write down the type of our bindings ever since Week3. Inside the SML is an algorithm called type inference that figures out the type of the bindings for us. It may sound magic for the first time, but in this week, Dan explained this mechanics for us.

The central idea of this algorithm is do assumptions and deductions as we go. It exams the bindings from top to bottom and every time a new thing comes up it first assumes that it is a new type and then infers its type by collecting facts associated with it. Here is an example:

1
2
3
4
fun f x =
  let val (y, z) = x in
    (abs y) + z
  end

The whole inference process goes like this:

  1. Looking at the first line, this is a function binding. So f has type T1->T2 for being a function. And x has type T1 for being the only parameter of f.
  2. Looking at the second line, x must have type T3*T4 for the pattern matching to type check. Also, y has type T3 and z has type T4.
  3. Examing the third line. We know from the standard library abs has type int->int. So T3=int. z must also have type int because only int can be added to int. So T4=int.
  4. Looking at the last line, the whole let expression ends with an addition. So the type of the let expression is int. Thus the type of the returned value of f is int.
  5. Combining all the facts together and concluding that f has type int*int->int.

Now type inference may seem more easy and simple. But to have type inference in a programming language requires delicate design. SML is well designed to have a good type inference algorithm. Some of the programming languages does not even have a feasible type inference algorithm. A feasible type inference algorithm must do the following three things:

  • Always terminate
  • Accept all the programs that type check and give the right type
  • Reject all the programs that does not type check

The question of how difficult the type inference algorithm is does not have a clear relation with how permissive the type system of the language is. For example, the type system that accepts everything and the type system that rejects everything are both easy to type check and type infer. Actually, to make the type inference in SML more difficult, we only need small modification to the type system of SML.

  1. If we admit subtyping(e.g., if every triple can also be a pair), the type inference will be much more difficult because we cannot reach the conclusion x has type T1*T2 with the pattern matching (y, z) = x. x may have two, three or more fields.
  2. If we disallow polymophic types, the type inference will also be more difficult because the type inference algorithm has to choose one concrete type which depends on the use of the binding.

    Value Restriction

    Another thing worth mentioning about type inference is value restriction. This mechanic is introduced to prevent typical invalid use of reference in SML, like the following:
    1
    2
    3
    val r = ref NONE       (* 'a option ref *)
    val _ = r := SOME "hi" (* instantiate 'a with string *)
    val i = 1 + valOf(!r)  (* instantiate 'a with int *)

With the type inference and type checking system so far, the code above is type check, though it should not. The solution SML presents is stopping the first line from type checking by forbidding a variable(val binding) to have polymophic type from functions. Actually, SML only allows val bindings to have polymophic type when the expression is a value or another variable.

The solution is effective but sometimes burdensome. For example, in Week4 we have partial application. One mysterious compilation problem is that we cannot use val bindings to hold polymophic typed fucntion generated by partial application. The reason turns out to be value restriction.

So there is also an interesting question: why don’t we just do this restriction for ref? The answer is sometimes the compiler cannot make sure that one type is a ref type with the existence of type synonym and signature. Type synonym may make this decision about whether a type is a ref type harder. Even worse, signature can make this decision impossible by hiding the type from clients.

Equivalence

Equivalence is an important topic of software developing. As time goes by, the code change, but the function of the code may need to stay all the same. This may happen when we refactor or improve our code without changing the existing features.

Dan presents a commonly used definition about equivalence between fucntions. To claim that two functions are the same, we need them to do the following when given the same parameters in the same environment:

  • Produce the same result
  • Have the same (non)termination behavior
  • Mutate the same memory in the same way
  • Do the same input/output
  • Raise the same exception

In this definition, we need two equivalent functions to produce the same result and have the same side effect. But the internal implementation does not concern us. Nor does the efficiency of the implementation. All those are assumed as unobservable. This is good because we need to replace some inferior implementation with some better one and claim they are equivalent.

But we also have other perspectives, like the asymptotic complexity in algorithm analysis and the actual performence in real projects. All these are valuable and useful.

Dan also presents some standard equivalence in Week5. But on my opinion, those examples only serve to clarify the definition of equivalence. They does not help in real software developing. Most of the standard equivalence are syntax tricks. But here is one interesting thing—let val p = e1 in e2 end is equivalent(syntactic sugar) for (fn p => e2) e1.