iconmaster5326 · October 19, 2018 23:30 · May 30, 2018 · May 30, 2018 · May 30, 2018 · May 30, 2018
diff --git a/catacomb.md b/catacomb.md
@@ -67,6 +67,25 @@ UNIFY (-- Int Int {Int Int -- Real}) AND (A {A -- B} -- B; *A; *B):
         -- Real
 ```
 
+```
+UNIFY (-- {Int -- Real}) AND ({Int Int -- Int Real} --):
+    CONSTRAINTS:
+        MATCH {Int -- Real} = {Int Int -- Int Real}
+            Int = Int Int
+            Real = Int Real
+            INVALID
+        MATCH {A Int -- A Real} = {Int Int -- Int Real}; A = All*
+            A Int = Int Int
+            A Real = Int Real
+            A = Int
+            VALID
+        WE KNOW:
+            A = Int;
+        FINALLY:
+            --
+            --
+```
+
 ## Problems
 
 Function expansion of `{a--b}` to `{c a--c b}` is nice and all, and accurately reflects how functions work, but is it sound inside composition? Does it generate cases where the type signature informs the behavior of the function? That would be bad.
diff --git a/catacomb.md b/catacomb.md
@@ -21,7 +21,8 @@ It can also be equivalenty seen as the composition of two functions' execution.
     * `A = B` and `B = C` to `A = C`
     * `A = B` to `B = A` (maybe? Is this an equality or subtyping relation?)
     * `A = B A` to `B = `
-    * `A B = C D` to `A = C` and `B = D` IFF they're all finite types
+    * `A B = C D` to `A = C` IFF `B` and `D` are finite types
+    * `A B = C D` to `B = D` IFF `A` and `C` are finite types
     * `A B C = D` and `B = E` to `A E C = D` (an extension of the transitive property above)
     * `A B = A C` to `B = C`
 5. Find the combined signature of the first unification that succeeds.

diff --git a/catacomb.md b/catacomb.md
@@ -23,6 +23,7 @@ It can also be equivalenty seen as the composition of two functions' execution.
     * `A = B A` to `B = `
     * `A B = C D` to `A = C` and `B = D` IFF they're all finite types
     * `A B C = D` and `B = E` to `A E C = D` (an extension of the transitive property above)
+    * `A B = A C` to `B = C`
 5. Find the combined signature of the first unification that succeeds.
    If you unify `a -- b x` and `c x -- d`, where `x` is the matched portion and `b/c` are unmatched ones, you get
    `c a -- b d`. Note that either `b` or `c` must be empty because of how matching works.

diff --git a/catacomb.md b/catacomb.md
@@ -6,9 +6,9 @@ It can also be equivalenty seen as the composition of two functions' execution.
 1. Generate constraints from the stated type sigs of your functions.
 2. Match the RHS of the LHF, and the LHS of the RHF, from right to left. If the two symbols are:
     * Base types: Fail if one is not a parent type of the other. Otherwise, move on.
-    * Both function types: Recursively generate constraints, starting with `{a} = {b}`
-      and expanding the functions using the function expansion rule, `{a--b}` -> `{c a--c b}`,
-      until one constraint set successfully unifies. If nothing works, fail.
+    * Both function types: Add a constraint `{a -- b} = {c -- d}` and run step (4) early.
+      If this produces an invalid constraint, try again by introducing a new variable `x`
+      and adding constraints `{x a -- x b} = {c -- d}` and `x = All*` instead of the original one.
     * One is a variardic type: Run step (4) early to figure out the type of your variaric type.
       It should always be determinable from here (because finite types always come first).
       Expand the variadic type in question in-place, and try matching again.

diff --git a/catacomb.md b/catacomb.md
@@ -11,7 +11,7 @@ It can also be equivalenty seen as the composition of two functions' execution.
       until one constraint set successfully unifies. If nothing works, fail.
     * One is a variardic type: Run step (4) early to figure out the type of your variaric type.
       It should always be determinable from here (because finite types always come first).
-      Consume the types on the other side your type results in, or fail if you cannot.
+      Expand the variadic type in question in-place, and try matching again.
     * Else: generate a constraint `a = b` and move on.
 3. When one side runs out of symbols, you can divide the other side into its matched and unmatched symbols.
    Save these for step (5).

diff --git a/catacomb.md b/catacomb.md
@@ -58,7 +58,6 @@ UNIFY (-- Int Int {Int Int -- Real}) AND (A {A -- B} -- B; *A; *B):
         MATCH {Int Int -- Real} = {A -- B}
         Int Int = A
         Real = B
-        MATCH Int Int = A
     WE KNOW:
         A = Int Int; B = Real;
     FINALLY:

diff --git a/catacomb.md b/catacomb.md
@@ -9,7 +9,9 @@ It can also be equivalenty seen as the composition of two functions' execution.
     * Both function types: Recursively generate constraints, starting with `{a} = {b}`
       and expanding the functions using the function expansion rule, `{a--b}` -> `{c a--c b}`,
       until one constraint set successfully unifies. If nothing works, fail.
-    * One is a variardic type: Move past the variardic types until both symbols being compared are finite ones.
+    * One is a variardic type: Run step (4) early to figure out the type of your variaric type.
+      It should always be determinable from here (because finite types always come first).
+      Consume the types on the other side your type results in, or fail if you cannot.
     * Else: generate a constraint `a = b` and move on.
 3. When one side runs out of symbols, you can divide the other side into its matched and unmatched symbols.
    Save these for step (5).
@@ -26,15 +28,15 @@ It can also be equivalenty seen as the composition of two functions' execution.
    `c a -- b d`. Note that either `b` or `c` must be empty because of how matching works.
 6. For each type variable, find all the consrtaints the mention it and find the most specific type among them. Replace.
 
-## Example
+## Examples
 
 ```
 UNIFY (-- {(?) -- Int?Int}.) AND (C A {C A -- C A?B} -- C B; *A; *B; *C.):
     CONSTRAINTS:
         A = All*
         B = All*
         C = All*
-        {(?) -- (?)?Int} = {C A -- C A?B}
+        MATCH {(?) -- (?)?Int} = {C A -- C A?B}
         (?) = C A
         (?)?Int = A?B
         (?) = A
@@ -48,6 +50,22 @@ UNIFY (-- {(?) -- Int?Int}.) AND (C A {C A -- C A?B} -- C B; *A; *B; *C.):
         (?) -- Int
 ```
 
+```
+UNIFY (-- Int Int {Int Int -- Real}) AND (A {A -- B} -- B; *A; *B):
+    CONSTRAINTS:
+        A = All*
+        B = All*
+        MATCH {Int Int -- Real} = {A -- B}
+        Int Int = A
+        Real = B
+        MATCH Int Int = A
+    WE KNOW:
+        A = Int Int; B = Real;
+    FINALLY:
+        -- B
+        -- Real
+```
+
 ## Problems
 
 Function expansion of `{a--b}` to `{c a--c b}` is nice and all, and accurately reflects how functions work, but is it sound inside composition? Does it generate cases where the type signature informs the behavior of the function? That would be bad.
diff --git a/catacomb.md b/catacomb.md
@@ -7,7 +7,7 @@ It can also be equivalenty seen as the composition of two functions' execution.
 2. Match the RHS of the LHF, and the LHS of the RHF, from right to left. If the two symbols are:
     * Base types: Fail if one is not a parent type of the other. Otherwise, move on.
     * Both function types: Recursively generate constraints, starting with `{a} = {b}`
-      and expanding the functions using the function expansion rule: `{a--b}` -> `{c a--c b}`.
+      and expanding the functions using the function expansion rule, `{a--b}` -> `{c a--c b}`,
       until one constraint set successfully unifies. If nothing works, fail.
     * One is a variardic type: Move past the variardic types until both symbols being compared are finite ones.
     * Else: generate a constraint `a = b` and move on.

diff --git a/catacomb.md b/catacomb.md
@@ -7,7 +7,7 @@ It can also be equivalenty seen as the composition of two functions' execution.
 2. Match the RHS of the LHF, and the LHS of the RHF, from right to left. If the two symbols are:
     * Base types: Fail if one is not a parent type of the other. Otherwise, move on.
     * Both function types: Recursively generate constraints, starting with `{a} = {b}`
-      and expanding the functions using the rule `{--} ==> {a -- a}`
+      and expanding the functions using the function expansion rule: `{a--b}` -> `{c a--c b}`.
       until one constraint set successfully unifies. If nothing works, fail.
     * One is a variardic type: Move past the variardic types until both symbols being compared are finite ones.
     * Else: generate a constraint `a = b` and move on.

diff --git a/catacomb.md b/catacomb.md
@@ -50,4 +50,4 @@ UNIFY (-- {(?) -- Int?Int}.) AND (C A {C A -- C A?B} -- C B; *A; *B; *C.):
 
 ## Problems
 
-Function expansion of `{--}` to `{a--a}` is nice and all, but is it sound? Does it generate cases where the type signature informs the behavior of the function? That would be bad.
+Function expansion of `{a--b}` to `{c a--c b}` is nice and all, and accurately reflects how functions work, but is it sound inside composition? Does it generate cases where the type signature informs the behavior of the function? That would be bad.
diff --git a/catacomb.md b/catacomb.md
@@ -47,3 +47,7 @@ UNIFY (-- {(?) -- Int?Int}.) AND (C A {C A -- C A?B} -- C B; *A; *B; *C.):
         C A -- C B
         (?) -- Int
 ```
+
+## Problems
+
+Function expansion of `{--}` to `{a--a}` is nice and all, but is it sound? Does it generate cases where the type signature informs the behavior of the function? That would be bad.
diff --git a/catacomb.md b/catacomb.md
@@ -9,12 +9,18 @@ It can also be equivalenty seen as the composition of two functions' execution.
     * Both function types: Recursively generate constraints, starting with `{a} = {b}`
       and expanding the functions using the rule `{--} ==> {a -- a}`
       until one constraint set successfully unifies. If nothing works, fail.
-    * Both are choice types: decompose `A?B = C?D;` into `A = C; B = D;` and move on.
     * One is a variardic type: Move past the variardic types until both symbols being compared are finite ones.
     * Else: generate a constraint `a = b` and move on.
 3. When one side runs out of symbols, you can divide the other side into its matched and unmatched symbols.
    Save these for step (5).
-4. Compute the closure of the constraint set.
+4. Compute the closure of the constraint set. Here are some basic rules:
+    * `{A -- B} = {C -- D}` to `A = C` and `B = D`
+    * `A?B = C?D` to `A = C` and `B = D`
+    * `A = B` and `B = C` to `A = C`
+    * `A = B` to `B = A` (maybe? Is this an equality or subtyping relation?)
+    * `A = B A` to `B = `
+    * `A B = C D` to `A = C` and `B = D` IFF they're all finite types
+    * `A B C = D` and `B = E` to `A E C = D` (an extension of the transitive property above)
 5. Find the combined signature of the first unification that succeeds.
    If you unify `a -- b x` and `c x -- d`, where `x` is the matched portion and `b/c` are unmatched ones, you get
    `c a -- b d`. Note that either `b` or `c` must be empty because of how matching works.

diff --git a/catacomb.md b/catacomb.md
@@ -14,7 +14,7 @@ It can also be equivalenty seen as the composition of two functions' execution.
     * Else: generate a constraint `a = b` and move on.
 3. When one side runs out of symbols, you can divide the other side into its matched and unmatched symbols.
    Save these for step (5).
-4. Solve constraints.
+4. Compute the closure of the constraint set.
 5. Find the combined signature of the first unification that succeeds.
    If you unify `a -- b x` and `c x -- d`, where `x` is the matched portion and `b/c` are unmatched ones, you get
    `c a -- b d`. Note that either `b` or `c` must be empty because of how matching works.

diff --git a/catacomb.md b/catacomb.md
@@ -7,8 +7,9 @@ It can also be equivalenty seen as the composition of two functions' execution.
 2. Match the RHS of the LHF, and the LHS of the RHF, from right to left. If the two symbols are:
     * Base types: Fail if one is not a parent type of the other. Otherwise, move on.
     * Both function types: Recursively generate constraints, starting with `{a} = {b}`
-    and expanding the functions using the rule `{--} ==> {a -- a}`
-	until one constraint set successfully unifies. If nothing works, fail.
+      and expanding the functions using the rule `{--} ==> {a -- a}`
+      until one constraint set successfully unifies. If nothing works, fail.
+    * Both are choice types: decompose `A?B = C?D;` into `A = C; B = D;` and move on.
     * One is a variardic type: Move past the variardic types until both symbols being compared are finite ones.
     * Else: generate a constraint `a = b` and move on.
 3. When one side runs out of symbols, you can divide the other side into its matched and unmatched symbols.

diff --git a/catacomb.md b/catacomb.md
@@ -11,13 +11,13 @@ It can also be equivalenty seen as the composition of two functions' execution.
 	until one constraint set successfully unifies. If nothing works, fail.
     * One is a variardic type: Move past the variardic types until both symbols being compared are finite ones.
     * Else: generate a constraint `a = b` and move on.
-When one side runs out of symbols, you can divide the other side into its matched and unmatched symbols.
-Save these for step (4).
-3. Solve constraints.
-4. Find the combined signature of the first unification that succeeds.
+3. When one side runs out of symbols, you can divide the other side into its matched and unmatched symbols.
+   Save these for step (5).
+4. Solve constraints.
+5. Find the combined signature of the first unification that succeeds.
    If you unify `a -- b x` and `c x -- d`, where `x` is the matched portion and `b/c` are unmatched ones, you get
    `c a -- b d`. Note that either `b` or `c` must be empty because of how matching works.
-5. For each type variable, find all the consrtaints the mention it and find the most specific type among them. Replace.
+6. For each type variable, find all the consrtaints the mention it and find the most specific type among them. Replace.
 
 ## Example
 

diff --git a/catacomb.md b/catacomb.md
@@ -11,8 +11,8 @@ It can also be equivalenty seen as the composition of two functions' execution.
 	until one constraint set successfully unifies. If nothing works, fail.
     * One is a variardic type: Move past the variardic types until both symbols being compared are finite ones.
     * Else: generate a constraint `a = b` and move on.
-   When one side runs out of symbols, you can divide the other side into its matched and unmatched symbols.
-   Save these for step (4).
+When one side runs out of symbols, you can divide the other side into its matched and unmatched symbols.
+Save these for step (4).
 3. Solve constraints.
 4. Find the combined signature of the first unification that succeeds.
    If you unify `a -- b x` and `c x -- d`, where `x` is the matched portion and `b/c` are unmatched ones, you get

diff --git a/catacomb.md b/catacomb.md
@@ -9,10 +9,10 @@ It can also be equivalenty seen as the composition of two functions' execution.
     * Both function types: Recursively generate constraints, starting with `{a} = {b}`
     and expanding the functions using the rule `{--} ==> {a -- a}`
 	until one constraint set successfully unifies. If nothing works, fail.
-    * One is a variardic type: Recursively generate constraints, starting with `a = `
-    and epanding the constraint to capture more values on the other side
-    until one constraint set successfully unifies. If nothing works, move on.
+    * One is a variardic type: Move past the variardic types until both symbols being compared are finite ones.
     * Else: generate a constraint `a = b` and move on.
+   When one side runs out of symbols, you can divide the other side into its matched and unmatched symbols.
+   Save these for step (4).
 3. Solve constraints.
 4. Find the combined signature of the first unification that succeeds.
    If you unify `a -- b x` and `c x -- d`, where `x` is the matched portion and `b/c` are unmatched ones, you get
@@ -21,23 +21,22 @@ It can also be equivalenty seen as the composition of two functions' execution.
 
 ## Example
 
-Let's compose `-- {Int --}` and `a {a --} -- a; All* a`.
-
-1. Our inital constraint set is `a = All*`.
-2. We're matching `{Int --}` with `a {a --}`. We compare `{Int --}` with `{a --}`.  This causes a sub-constraint-solve, starting with no expansions:
-    1. `{Int --} = {a --}` is added to our constraints (also producing rules like `Int = a`).
-    2. We next match ` ` with `a`. This causes a sub-constraint-solve:
-        1. `a = `. This fails because `Int = ` is unsolvable.
-        2. Nothing worked, and we have no symbols to consume, so we add no constrants and move on.
-           Luckily, this succeeds.
-3. We've found a set of constraints that cause no issues: `a = All*; Int = a`.
-4. For `a`, the common type among `All*` and `Int` is `Int`.
-5. The un-expanded composition type is `a -- a`. Substituted, our answer is `Int -- Int`.
-
-## Problems
-
-Using this method, the type signature of a function suddenly influences how the function operates - A function with a silly signature such as `{a -- b} a -- b` suddenly knows how many arguments to take as `a` in every situation, despite not knowing where the function is relative to the latter arguments, for example.
-
-This is bad. Here might be a simpler (yet less robust) composition method:
-* Finite arguments must ALWAYS come before indefinite ones.
-* No function expansion. `{--}` to `{a -- a}` is dangerous.
+```
+UNIFY (-- {(?) -- Int?Int}.) AND (C A {C A -- C A?B} -- C B; *A; *B; *C.):
+    CONSTRAINTS:
+        A = All*
+        B = All*
+        C = All*
+        {(?) -- (?)?Int} = {C A -- C A?B}
+        (?) = C A
+        (?)?Int = A?B
+        (?) = A
+        Int = B
+        (?) = C (?)
+        C = 
+    WE KNOW:
+        A = (?); B = Int; C = ;
+    FINALLY:
+        C A -- C B
+        (?) -- Int
+```
diff --git a/catacomb.md b/catacomb.md
@@ -32,4 +32,12 @@ Let's compose `-- {Int --}` and `a {a --} -- a; All* a`.
            Luckily, this succeeds.
 3. We've found a set of constraints that cause no issues: `a = All*; Int = a`.
 4. For `a`, the common type among `All*` and `Int` is `Int`.
-5. The un-expanded composition type is `a -- a`. Substituted, our answer is `Int -- Int`.
+5. The un-expanded composition type is `a -- a`. Substituted, our answer is `Int -- Int`.
+
+## Problems
+
+Using this method, the type signature of a function suddenly influences how the function operates - A function with a silly signature such as `{a -- b} a -- b` suddenly knows how many arguments to take as `a` in every situation, despite not knowing where the function is relative to the latter arguments, for example.
+
+This is bad. Here might be a simpler (yet less robust) composition method:
+* Finite arguments must ALWAYS come before indefinite ones.
+* No function expansion. `{--}` to `{a -- a}` is dangerous.
diff --git a/catacomb.md b/catacomb.md
@@ -1,16 +1,35 @@
+# Composition
+
 **Composition** is the act of taking a stack and a function, and producing the type signature of the resulting stack.
 It can also be equivalenty seen as the composition of two functions' execution.
 
 1. Generate constraints from the stated type sigs of your functions.
 2. Match the RHS of the LHF, and the LHS of the RHF, from right to left. If the two symbols are:
-    * Base types: Fail if one is not a parent type of the other. Otherwise, do nothing.
+    * Base types: Fail if one is not a parent type of the other. Otherwise, move on.
     * Both function types: Recursively generate constraints, starting with `{a} = {b}`
     and expanding the functions using the rule `{--} ==> {a -- a}`
-	until one constraint set successfully unifies.
+	until one constraint set successfully unifies. If nothing works, fail.
     * One is a variardic type: Recursively generate constraints, starting with `a = `
     and epanding the constraint to capture more values on the other side
-    until one constraint set successfully unifies.
+    until one constraint set successfully unifies. If nothing works, move on.
     * Else: generate a constraint `a = b` and move on.
-3. Return the result of the first unification that succeeds.
+3. Solve constraints.
+4. Find the combined signature of the first unification that succeeds.
    If you unify `a -- b x` and `c x -- d`, where `x` is the matched portion and `b/c` are unmatched ones, you get
-   `c a -- b d`. Note that either `b` or `c` must be empty because of how matching works.
+   `c a -- b d`. Note that either `b` or `c` must be empty because of how matching works.
+5. For each type variable, find all the consrtaints the mention it and find the most specific type among them. Replace.
+
+## Example
+
+Let's compose `-- {Int --}` and `a {a --} -- a; All* a`.
+
+1. Our inital constraint set is `a = All*`.
+2. We're matching `{Int --}` with `a {a --}`. We compare `{Int --}` with `{a --}`.  This causes a sub-constraint-solve, starting with no expansions:
+    1. `{Int --} = {a --}` is added to our constraints (also producing rules like `Int = a`).
+    2. We next match ` ` with `a`. This causes a sub-constraint-solve:
+        1. `a = `. This fails because `Int = ` is unsolvable.
+        2. Nothing worked, and we have no symbols to consume, so we add no constrants and move on.
+           Luckily, this succeeds.
+3. We've found a set of constraints that cause no issues: `a = All*; Int = a`.
+4. For `a`, the common type among `All*` and `Int` is `Int`.
+5. The un-expanded composition type is `a -- a`. Substituted, our answer is `Int -- Int`.
diff --git a/catacomb.md b/catacomb.md
@@ -12,5 +12,5 @@ It can also be equivalenty seen as the composition of two functions' execution.
     until one constraint set successfully unifies.
     * Else: generate a constraint `a = b` and move on.
 3. Return the result of the first unification that succeeds.
-   If you unify `a -- b1 b2` and `c1 c2 -- d`, where `b1/c1` are unmatched portions and `b2/c2` are matched ones, you get
-   `a c1 -- b1 d`.
+   If you unify `a -- b x` and `c x -- d`, where `x` is the matched portion and `b/c` are unmatched ones, you get
+   `c a -- b d`. Note that either `b` or `c` must be empty because of how matching works.
diff --git a/catacomb.md b/catacomb.md
@@ -3,14 +3,14 @@ It can also be equivalenty seen as the composition of two functions' execution.
 
 1. Generate constraints from the stated type sigs of your functions.
 2. Match the RHS of the LHF, and the LHS of the RHF, from right to left. If the two symbols are:
-  * Base types: Fail if one is not a parent type of the other. Otherwise, do nothing.
-  * Both function types: Recursively generate constraints, starting with `{a} = {b}`
+    * Base types: Fail if one is not a parent type of the other. Otherwise, do nothing.
+    * Both function types: Recursively generate constraints, starting with `{a} = {b}`
     and expanding the functions using the rule `{--} ==> {a -- a}`
 	until one constraint set successfully unifies.
-  * One is a variardic type: Recursively generate constraints, starting with `a = `
+    * One is a variardic type: Recursively generate constraints, starting with `a = `
     and epanding the constraint to capture more values on the other side
     until one constraint set successfully unifies.
-  * Else: generate a constraint `a = b` and move on.
+    * Else: generate a constraint `a = b` and move on.
 3. Return the result of the first unification that succeeds.
    If you unify `a -- b1 b2` and `c1 c2 -- d`, where `b1/c1` are unmatched portions and `b2/c2` are matched ones, you get
    `a c1 -- b1 d`.
diff --git a/catacomb.md b/catacomb.md
@@ -0,0 +1,16 @@
+**Composition** is the act of taking a stack and a function, and producing the type signature of the resulting stack.
+It can also be equivalenty seen as the composition of two functions' execution.
+
+1. Generate constraints from the stated type sigs of your functions.
+2. Match the RHS of the LHF, and the LHS of the RHF, from right to left. If the two symbols are:
+  * Base types: Fail if one is not a parent type of the other. Otherwise, do nothing.
+  * Both function types: Recursively generate constraints, starting with `{a} = {b}`
+    and expanding the functions using the rule `{--} ==> {a -- a}`
+	until one constraint set successfully unifies.
+  * One is a variardic type: Recursively generate constraints, starting with `a = `
+    and epanding the constraint to capture more values on the other side
+    until one constraint set successfully unifies.
+  * Else: generate a constraint `a = b` and move on.
+3. Return the result of the first unification that succeeds.
+   If you unify `a -- b1 b2` and `c1 c2 -- d`, where `b1/c1` are unmatched portions and `b2/c2` are matched ones, you get
+   `a c1 -- b1 d`.
No results found