能否在函数外部使用`with`？能否在函数签名中直接使用views与`with`？

你尝试的写法不符合Idris语法规则：with是Idris为顶层函数定义提供的模式匹配扩展语法，不能直接嵌套在类型签名的case表达式中。不需要额外定义类型级函数，就可以实现你要的view匹配逻辑，正确实现方式如下：

直接在函数定义中使用with #

import Data.List.Views

data Foo : List Nat -> Type where
  -- 可根据需求补充Foo的构造子定义
  MkFoo : Foo xs

bar : Foo xs -> Nat -- 这里换成你实际需要的返回类型
bar xs with (snocList xs)
  bar xs | Empty => ?rhs_empty
  bar xs | Snoc y ys rec => ?rhs_snoc

在let代码块中使用view匹配 #

如果你不想用with语法，也可以直接在let中绑定view结果再做模式匹配：

bar : Foo xs -> Nat
bar xs = let snocView = snocList xs in
  case snocView of
    Empty => ?rhs_empty
    Snoc y ys rec => ?rhs_snoc

返回类型依赖匹配结果的实现 #

如果你的函数返回类型需要根据列表拆分结果变化，直接使用依赖case即可，不需要额外定义独立的类型级函数：

bar : Foo xs -> (snoc : SnocList xs) -> case snoc of
  Empty => Nat -- 空列表场景的返回类型
  Snoc y ys rec => Int -- 非空snoc结构场景的返回类型
bar xs snoc with (snocList xs)
  bar xs snoc | Empty = 0
  bar xs snoc | Snoc y ys rec = 1

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