如何在Idris2中定义签名，实现线性Haskell式maybeToList的合规行为？

我认为maybeToList是尝试Idris2线性特性的合适函数。我知道maybeToVect通常是更优选择，但推测其实现不会采用“线性使用容器中所有a”的方式。在线性Haskell中，maybeToList :: Maybe a %1 -> [a]要求线性使用Just x中的x，但在Idris2中，以下错误实现却能通过类型检查：

maybeToList : (1 _ : Maybe a) -> List a
maybeToList (Just x) = []
maybeToList Nothing = []

同时，idris-boot中的maybeToVect签名也允许错误实现通过类型检查：

maybeToVect : Maybe elem -> (p ** Vect p elem)
maybeToVect Nothing  = (_ ** [])
maybeToVect (Just j) = (_ ** [j])

请问在Idris2中，我可以使用什么签名来实现与线性Haskell中相同的行为？

要在Idris2中实现和线性Haskell中maybeToList相同的线性约束效果，你需要同时约束容器本身的线性性，以及容器内部元素的线性性，并且确保输出的集合也以线性方式使用元素。

1. 修正maybeToList的签名 #

原签名仅约束了Maybe a整体是线性的，但没有约束内部的a必须被线性消耗。你需要将内部的a也标记为线性，同时让输出的List a也保持线性：

maybeToList : (1 _ : Maybe (1 a)) -> (1 _ : List a)

此时如果再写错误实现：

maybeToList (Just x) = []
maybeToList Nothing = []

Idris2会报错，因为线性标记的x未被使用，强制你必须将x包含在输出列表中，正确实现应为：

maybeToList (Just x) = [x]
maybeToList Nothing = []

2. 修正maybeToVect的签名 #

同理，要让maybeToVect满足线性约束，需要给输入的Maybe elem和内部的elem加上线性标记，同时确保输出的Vect也是线性的：

maybeToVect : (1 _ : Maybe (1 elem)) -> (p ** (1 _ : Vect p elem))

这个签名会强制你在处理Just j时，必须将j放入输出的Vect中，否则会因线性变量未被使用而触发类型检查错误。

核心原因 #

Idris2的线性类型标记是逐变量生效的：原签名中的(1 _ : Maybe a)仅要求整个Maybe值被线性使用（即不能被重复使用或丢弃），但不约束内部的a。通过把内部元素也标记为1 a，我们明确要求这个元素必须被线性消耗——要么放入输出容器，要么被显式销毁（Idris2中默认不允许未使用的线性变量）。

内容的提问来源于stack exchange，提问作者Johannes Riecken