如何让Idris取消映射矢量以推断类型？

Question

我有以下工作职能:

unMaybe : (t : Type) -> {auto p : t = Maybe x} -> Type
unMaybe {x} _ = x

这个功能很好用:

> unMaybe (Maybe Int)
Int

我还有另一个类似的功能:

unMaybesA : (ts : Vect n Type) -> {xs : Vect n Type} -> {auto p : map Maybe xs = ts} -> Vect n Type
unMaybesA {xs} _ = xs

不幸的是,以下失败:

> unMaybesA [Maybe Int, Maybe String]

(input):1:1-35:When checking argument p to function Main.unMaybesA:
        Can't find a value of type
                Data.Vect.Vect n implementation of Prelude.Functor.Functor, method map Maybe
                                                                                       xs =
                [Maybe Int, Maybe String]

但以下工作:

> unMaybesA {xs=[_,_]} [Maybe Int, Maybe String]
[Int, String]

这是一种让Idris能够自动{xs=[_,_]}处理_矢量的方法吗？

unMaybesB : (ts : Vect n Type) -> {auto p : (xs : Vect n Type ** map Maybe xs = ts)} -> Vect n Type
unMaybesB {p} _ = fst p

可能通过使用elaborator脚本在上面的函数中自动填充p？

我在下面列出了一个详细的脚本.我只需要弄清楚如何从目标中生成n,ts和xs.

helper1 : Vect n Type -> Vect n Type -> Type
helper1 ts xs = (map Maybe xs) = ts

unMaybesC : (ts : Vect n Type) -> {auto p : DPair (Vect n Type) (helper1 ts)} -> Vect n Type
unMaybesC {p} _ = fst p

helper2 : (n : Nat) -> (ts : Vect n Type) -> (xs : Vect n Type) -> helper1 ts xs -> DPair (Vect n Type) (helper1 ts)
helper2 _ _ xs p = MkDPair xs p

q : Elab ()
q = do
    let n = the Raw `(2 : Nat)
    let ts = the Raw `(with Vect [Maybe String, Maybe Int])
    let xs = the Raw `(with Vect [String, Int])
    fill `(helper2 ~n ~ts ~xs Refl)
    solve

qC : Vect 2 Type
qC = unMaybesC {p=%runElab q} [Maybe String, Maybe Int]

Answer 1

map Maybe xs = ts看似惯用,但很难.如果要auto搜索非简单证明,请编写显式证明类型.然后,证明搜索将尝试构造函数并在正确的方向上引导.

data IsMaybes : Vect n Type -> Vect n Type -> Type where
  None : IsMaybes [] []
  Then : IsMaybes xs ms -> IsMaybes (t :: xs) (Maybe t :: ms)

unMaybes : (ts : Vect n Type) -> {xs : Vect n Type} -> {auto p : IsMaybes xs ts} -> Vect n Type
unMaybes ts {xs} = xs

有了这个:

> unMaybes [Maybe Nat, Maybe Int, Maybe (Maybe String)]
[Nat, Int, Maybe String] : Vect 3 Type