[General boards] [Fall 2018 courses] [Summer 2018 courses] [Winter 2018 courses] [Older or newer terms]

A bit confused with Polish Notation, and other things


#1

I am a little confused about the appropriate usage of Polish Notation, (Though I believe it won’t be on the test?)
I will give an example computation to show my understanding, correct me if I do anything wrong:
if f,g : int -> int, h : int -> int -> int, x : int;
h f g x
= (((h f) g) x) (f not in domain of h, interpret it as composition)
= ((h (f g)) x) ((f g) is not in domain of h, interpret it as composition)
= (h ((f g) x)) (g not in domain of f, interpret it as composition)
=(h (f (g x)))

Q1: I don’t remember we have introduce the associativity of (right-)arrow, it is right-associative, correct?
Q2: Any two function, (as long as the one being ‘applied’ is not in domain) can be composed, correct? Even they are not ‘connected’, for example, f: A -> B, g : C -> D, can compose
Q3: How to (Can we) composite two function when the applied one is in the domain of the other?
Q4: if f,g: int -> int, h : (int -> int) -> int, can I write down “h f g”? (I mean the way I want to combine them is that (h (f g))
Q5: What do you think of Type Theory? Mainly, those type systems used by those functional programming languages? For example, Haskell (extended System F) and Coq (Calculus of Inductive Construction). I see that you interpret the notation “int -> int” as a non-deterministic function, and now the “:” is so general that it can be even used to express subtype and typing. Also there is “A: [3*[4 * nat]]” which is only supported in dependent type. What do you think of these theories compared to the theory we are learning?


#2

These questions are about function fine points, and you won’t be tested on them.

Q1 The final page of the textbook lists associativities. It says → associates from right to left.

Q2 Yes, if f is not in the domain of g, then g f is a composition. Suppose f:int→int and g:bin→bin. Then g f is a composed function, and its domain is §x:int· fx:bin. So its domain is empty. So it’s not a useful function.

Q3 I did not provide a notation for the composition of functions g and f where f is in the domain of g. Suppose f:A→B and g:(A→B)→C. Now f is in the domain of g. The domain of (g composed with f) would be §x:A· fx:A→B. So the domain of the composition is empty. So this composition is not useful. In Q2, there is a notation for the composition, not because I wanted it, but because it just comes along with all the useful compositions, and I saw no reason to exclude it. Here in Q3, I would need a new composition notation, and since these compositions are not useful, I did not provide a notation.

Q4 You can write h f g, which associates as (h f) g, and since h does apply to f, that’s application, not composition, so it’s not the same as (h (f g)).

Q5 Even with very simple types, type-checking is a very simple kind of limited correctness proof. With more elaborate types, type-checking is a little less limited correctness proof, but still a distance to go. With a full type theory, type-checking can be a full correctness proof. But Haskell and Coq don’t do type-checking. They do type inference. In other words, they use the power of type theory to save you the work of stating types. This is convenient, but much less safe. All error detection depends on redundancy - saying things that could be inferred. By using type inference, they reduce error detection. In this course, we do full correctness proofs. Our types (bunches) are part of the computational language. We don’t distinguish types from values. See the sentence beginning “Type theory …” on page 211.


#3

RE: Q5
“Type theory duplicates all the operators of its value space: for each operation on values, there is a
corresponding operation on type spaces. By using bunches as types, this duplication is eliminated.”
While on a computer, different data are encoded into different representation. It is inevitable to use different versions of the operator to decode them.

Though Coq and Haskell both have the ability to infer type, while in real life, I don’t remember any programmer completely “rely” on them. When programming, I believe the Haskeller would recommend writing type clearly first, or you would confuse yourself about what you really want.

I think the issue to discuss here is whether the introduction of “type” is a advanced. Do you think whether the concept of “type” is useful or it is purely fancy but useless stuff?


#4

I think it is very very useful to say, for each variable introduced, what values you intend to be assignable. I would call that the “type” of the variable.