implicit - GADT数据构造函数参数如何在Idris中工作？

这是GADT，其中包含三个数据构造函数，这些构造函数定义了列表视图：

data SplitList : List a -> Type where
  SplitNil : SplitList []
  SplitOne : SplitList [x]
  SplitPair : (lefts : List a) -> (rights : List a) ->
              SplitList (lefts ++ rights)

我不理解SplitOne：[x]是哪里来的？在SplitNil中，它似乎只是一个常量值（Nil），它被馈送到SplitList，但是在SplitOne中，x是隐式参数吗？

最佳答案

我不是专家，但是由于没有其他人在回答：是的，第一行中的a也是如此：List a -> Type is short for {a : Type} -> List a -> Type。

通过类型推断，x必须具有类型a，因此[x] : List a和SplitList [x] : Type。
我不确定的是


此a是另一个隐式参数，因此完整类型签名为SplitOne : {a : Type} -> {x : a} -> SplitList [x]（如果是，其名称是否真的为a？），或者
它受第一行的a约束。


但是第一个对我来说更有意义。