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

Question

这是一个 GADT，其中包含三个定义 ListView 的数据构造函数:

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 是隐式参数吗？

Answer 1

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

根据类型推断，x 必须具有类型 a，因此 [x] :列出 a 和 SplitList [x] :键入。 我不确定的是是否

1. 这个 a 是另一个隐式参数，因此完整的类型签名为 SplitOne : {a : Type} -> {x : a} -> SplitList [x] (如果是这样，它的名字真的是a吗？)，或者

2. 它以某种方式受到第一行的 a 的约束。

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