Implicit Design

[WtzLAS]

Look at the comments

[WtzLAS]

f: (implicit A: Type, implicit B: Type, A) -> B

infer f("123")
    infer f = (implicit A: Type, implicit B: Type, A) -> B
    detect target is a ImplicitPi
    put `A: Type` in ctx
    
    infer f (implicit A) ("123")
        infer f (implicit A) = (implicit B: Type, A) -> B
        detect target is a ImplicitPi
        put `B: Type` in ctx
        
        infer f (implicit A) (implicit B) ("123")
            infer f (implicit A) (implicit B) = A -> B
            
            check "123": A
                infer "123" = String
                unify String A      =>      Solution { A = String }
                fulfill `A: Type` with String in ctx
            
            return f (implicit A) (implicit B) ("123"): B
        
        pulls `B: Type` out of ctx
        
        *****ERROR: B IS DROPPED WHILE BEING REFERENCED
        
        return f (implicit A) ("123"): B
    
    pulls `A: Type = String` out of ctx
    replace every A with String in B
    
    return B

这里的 B 应该怎么处理（尤其是*****ERROR处）？

可能方案：

1. 直接报错 B 未解出
2. 检测到 B 未 fulfilled 时 返回一个 (implicit B: Type) -> B

[LittleJianCH]

我觉得应该要扔回去一个 g: (implicit B: Type, B) -> String

[xieyuheng]

看一下：https://github.com/cicada-lang/cicada/issues/36

[xieyuheng]

infer of Ap must resolve all of its pattern variables in this infer.

[WtzLAS]

会选择「直接报错 B 未解出」。

implicit pi 中的变量如果只出现在 return type 中，就只能在 check 的时候求解，不能在 infer 的时候求解。

因为 insert 的 implicit ap 必须和 implicit fn 的顺序一致， curry f("123") 这个 application 之后已经没机会 insert 了。

这里可能没法infer，但是上下文可能还有机会，比如此时 let a: String = f("123") ，还是可以确定B的类型

[xieyuheng]

你这个例子是 check

[WtzLAS]

Id: (implicit A: Type) -> A -> A
Nil: (implicit A: Type) -> List A
Cons: (implicit A: Type) -> A -> List A -> List A

check Cons(Id, Nil): List ({A} -> A -> A) {
    infer Cons(Id, Nil) {
        infer Cons {
            return ({A} -> A -> List A -> List A)
        }
        
        * last infer returned ImplicitPi
        * new `A: Type` in ctx
        
        infer Cons(implicit A)(Id, Nil) {
            infer Cons(implicit A) {
                return (A -> List A -> List A)
            }
            
            check Id: A {
                infer Id {
                    return (T_Id)
                    // T_Id = {A} -> A -> A
                    // the implicit arg A in this type is not inserted into ctx, so we write T_id here to avoid ambiguity
                }
                
                unify T_Id A {
                    return Solution { A = T_Id }
                }
                
                * fulfill A with T_Id in ctx
            }
            
            infer Cons(implicit A, Id)(Nil){
                infer Cons(implicit A, Id) {
                    return (List A -> List A)
                }
                
                check Nil: List A {
                    infer Nil {
                        return T_Nil // same as above
                    }
                    
                    unify T_Nil (List A) // ???
                }
            }
        }
    }
}

最后一个 check 里面的 unify 该如何处理？

现有的想法可能是 infer argType的时候得到 ImplicitPi 也要新建变量把 implicit args 消除

[xieyuheng]

这里两个例子用了不同的语法，感觉制造了没必要的理解困难。

为了方便读者理解，建议之后的讨论中，多个例子用一致的语法。

另外，除非是分析别的语言例子与 feature，
建议像第二个例子一样直接用 cicada 的语法。

[LittleJianCH]

所以现在 infer 和 check 的函数类型应该是什么

[WtzLAS]

现在没有加入metacontext的想法

[LittleJianCH]

那 Solution 也不需要吗

[WtzLAS]

不需要，拿到Solution之后直接将对应的ctx fulfill掉
但是如果原来已经fulfilled了可能要判断一下最大公共类型这样的东西

[LittleJianCH]

有种把 metacontext 和 context 合在一起的感觉

我不太清楚行不行

[WtzLAS]

不知道，只要能分得清就行，应该是没问题的

[WtzLAS]

能不能给Core加入ImplicitPi和ImplicitAp
First-Class Implicit Function Types
这才是first-class嘛

[WtzLAS]

Id: (implicit A: Type) -> A -> A
Nil: (implicit A: Type) -> List A
Cons: (implicit A: Type) -> A -> List A -> List A

check Cons(Id, Nil): List ((implicit A': Type) -> A' -> A') {
    infer Cons(Id, Nil) {
        infer Cons {
            return ((implicit A: Type) -> A -> List A -> List A), Cons
        }
        
        * new `A: Type` in metactx
        
        infer Cons(implicit A)(Id, Nil) {
            infer Cons(implicit A) {
                return (A -> List A -> List A), Cons(implicit A)
            }
            
            check Id: A {
                infer Id {
                    return (T_Id), Id
                    // T_Id = (implicit A: Type) -> A -> A
                    // the implicit arg A in this type is not inserted into ctx, so we write T_id here to avoid ambiguity
                }
                
                * new `M: Telescope` in metactx
                
                * new `B: Type` in metactx
                
--------------------------------!!!! Key Move !!!!-------------------------------------
|               Id(implicit B): (implicit M: Telescope) -> (B -> B)                   |
---------------------------------------------------------------------------------------
                
                unify A ((implicit M: Telescope) -> (B -> B)) {
                    return Solution { A = ((implicit M: Telescope) -> (B -> B)) }
                }
                
                * fulfill A with ((implicit M: Telescope) -> (B -> B)) in metactx
                
                return Id(implicit B)
            }
            
            infer Cons(implicit A, Id(implicit B))(Nil){
                infer Cons(implicit A, Id(implicit B)) {
                    return (List A -> List A), Cons(implicit A, Id(implicit B))
                }
                
                check Nil: List A {
                    infer Nil {
                        return T_Nil, Nil
                    }
                    
                    * new `C: Type` in metactx
                    
                    Nil(implicit C): List C
                    
                    unify (List C) (List A) {
                        return Solution { A = C }
                    }
                    
                    * fulfill C with A in metactx
                    
                    return Nil(implicit C)
                }
                
                return (List A), Cons(implicit A, Id(implicit B), Nil(implicit C))
            }
            
            return (List A), Cons(implicit A, Id(implicit B), Nil(implicit C))
        }
        
        return (List A), Cons(implicit A, Id(implicit B), Nil(implicit C))
    }
    
    unify (List A) (List ((implicit A': Type) -> A' -> A')) {
        List A = List ((implicit M: Telescope) -> (B -> B))
        
        unify List ((implicit M: Telescope) -> (B -> B)) (List ((implicit A': Type) -> A' -> A')) {
            * remove List, here omitted
            
            unify (M: Telescope) (A': Type) {
                * new `D: Telescope` in metactx
                
                return Solution { M.head = A', M.tail = D }
            }
            
            unify ((implicit D: Telescope) -> (B -> B)) (A' -> A') {
                unify D Telescope.Empty {
                    return Solution { D = Telescope.Empty }
                }
                
                unify (B -> B) (A' -> A') {
                    return Solution { B = A' }
                }
                
                return Solution { D = Telescope.Empty, B = A' }
            }
            
            return Solution { M.head = A', M.tail = D, D = Telescope.Empty, B = A' }
        }
        
        return Solution { M.head = A', M.tail = D, D = Telescope.Empty, B = A' }
    }
    
    check passed
}

这是根据ICFP20的论文改写的过程

[WtzLAS]

check "123": (implicit A: Type) -> String {
    check "123": String {
        return "123"
    }
    
    return (implicit A: Type) => "123"
}

可以看到这个check可以通过，并且插入了一个新的implicit abstraction

check "123": A {
    infer "123" {
        return String, "123"
    }
    
    unify String A {
        return Solution { A = String }
    }
    
    return "123"
}

但是像这样，check的右侧是一个在上下文中已经新建的variable，那么按照之前的算法会直接unify不会插入新implicit abstraction

但是这个A是可能在后来被 unify 到一个implicit function type的，因此在这种情况下无法推断
（比如后来进行了 unify A ((implicit B: Type) -> String)）

check "123": A {
    infer "123" {
        return String, "123"
    }
    
    * new `M: Telescope` in metactx
    * insert new implicit abstraction
    
    (implicit _: ...) => "123": (implicit M: Telescope) -> String
    
    // Telescope here means curried function
    
    unify ((implicit M: Telescope) -> String) A {
        return Solution { A = ((implicit M: Telescope) -> String)}
    }
    
    return (implicit _: ...) => "123"
}

ICFP20的论文改善了这里的行为，通过插入curried implicit abstraction (这里用Telescope表示) 来接受可能后来额外需要接受的implicit arg

此时 unify A ((implicit B: Type) -> String) 就会返回 Solution { M.head = B, M.rest = Telescope.Empty }