KimBruce
commented
8 years ago These should be fairly straightforward to prove (though I thought we weren’t actually writing “+” types in the syntax).
E.g. (A | B) & C <: (A & C) | (B & C)
Let D = (A | B) & C. Then D <: (A | B) and D <: C. But D <: (A | B) => D <: A or D <: B. Thus, D <: A & C or D <: B & C, and hence D <: (A & C) | (B & C).
The other direction just runs the proof backwards. Others (at least without +) should be similarly straightforward. I haven’t thought through the case of + as that likely involves assumptions on the lattice.
Show (A & B) | C = (A | C) & (B | C).
D = (A & B) | C => D <: A & B or D <: C. Two cases (i) D <: A & B. Therefore D <: A and D <: B. Thus D <: A | C and D <: B | C. Thus D <: (A | C) & (B | C). Case (ii) D <: C is trivial
Other direction.
Let D = (A | C) & (B | C). Thus D <: (A | C) and D <: (B | C). If D <: C then clearly D <: (A & B) | C. Suppose not. Thus D <: A and D <: B. Thus D <: A & B, and hence D <: (A & B) | C.
Let me know if I’ve overlooked something here. I remain concerned about combining | and +
Kim
On Feb 14, 2016, at 1:15 PM, Andrew Black notifications@github.com wrote:
I believe that it is true that any Grace type can be described as a list of variants, that is, as a a disjunction of interfaces. This is analogous to DNF for logical expressions.
More precisely, we can equate a single interface A to a disjunction with one element A, A | B to a single level disjunction, (A | B) | C and A | (B | C) to A | B | C, (A | B) & C to (A & C) | (B & C), (A | B) + C to (A + C) | (B + C), and so on. By "equate to" I mean that both expressions conform to each other.
If this is true, then we need to write down and prove these theorems. If it's not true, then we need to find out pretty darn quick (through being unable to prove the theorems, or finding a counterexample). It seems like this would be good material for someone writing a thesis on types.
Pragmatically, the minigrace dynamic type checking system gives up when it sees a variant type (one containing a |). These theorems would let me implement a normal form for types, and evaluate complex type expressions to that normal form.
— Reply to this email directly or view it on GitHub https://github.com/gracelang/language/issues/48.
kjx
I believe that it is true that any Grace type can be described as a list of variants, that is, as a a disjunction of interfaces. This is analogous to DNF for logical expressions.
More precisely, we can equate a single interface
Ato a disjunction with one elementA,A | Bto a single level disjunction,(A | B) | CandA | (B | C)toA | B | C,(A | B) & Cto(A & C) | (B & C),(A | B) + Cto(A + C) | (B + C), and so on. By "equate to" I mean that both expressions conform to each other.If this is true, then we need to write down and prove these theorems. If it's not true, then we need to find out pretty darn quick (through being unable to prove the theorems, or finding a counterexample). It seems like this would be good material for someone writing a thesis on types.
Pragmatically, the minigrace dynamic type checking system gives up when it sees a variant type (one containing a
|). These theorems would let me implement a normal form for types, and evaluate complex type expressions to that normal form.