统一len和S len会带来无限的价值

Question

我试图hpure通过重复相同的元素来生成一个生成hvect 的函数,直到达到所需的长度.每个元素可以具有不同的类型.例如:如果参数显示,则每个元素都是show函数的特化.

hpure show : HVect [Int -> String, String -> String, SomeRandomShowableType ->  String]

这是我的尝试:

hpure : {outs : Vect k Type} -> ({a : _} -> {auto p : Elem a outs} -> a) -> HVect outs
hpure {outs = []} _ = []
hpure {outs = _ :: _ } v = v :: hpure v

最终v发生此错误:

When checking an application of Main.hpure:
        Unifying len and S len would lead to infinite value

为什么会出现错误以及如何解决？

Answer 1

问题在于类型v依赖于outs,并且递归调用hpure传递尾部outs.所以也v需要调整.

该错误基本上是说,outs为了使你的版本能够进行类型检查,其长度和尾部必须相同.

这是一个typechecks的版本.

hpure : {outs : Vect k Type} -> ({a : Type} -> {auto p : Elem a outs} -> a) -> HVect outs
hpure {outs = []} _ = []
hpure {outs = _ :: _} v = v Here :: hpure (\p => v (There p))