时间戳

首页 > 解决方案 > Idris 中的“不可访问的模式变量”

functional-programming - Idris 中的“不可访问的模式变量”

问题描述

我遇到了一个问题，即 Idris 中的模式匹配给出“不可访问的模式变量”错误，即使我只是使用编译器来指导模式匹配。

这是我正在尝试做的一个例子。细节并不是非常重要，主要的是我有一些类似于向量的东西，除了它是通过向量索引之间的关系参数化的，而不是使用相等性。然后我得到了另一种定义关系的类型，其中一个变体是向量之间的关系 PC。（我的实际代码还有其他情况，我刚刚把它们删掉了）。

然后我试图通过在 PC 证明上进行模式匹配来定义一个函数“trans”。如果我执行“trans pf1 pf2 = ?foo”，那么它可以工作。但是，如果我区分大小写（使用编辑器命令来区分大小写），我会得到“nwhole 不是可访问的模式变量”。这对我来说似乎很奇怪，在一个类型检查的程序上执行编译器给定的大小写分割会产生一个没有的程序。而且，我不知道如何进行代码类型检查。

有谁知道这里发生了什么？这是一个错误，还是我的隐式参数/类型索引做错了什么？

module MinimalExample

data NNat = NNone | NZ | NSucc NNat

parameters (rel : NNat -> NNat -> Type )
  data PreVec : Type -> NNat -> Type where
    VNil : {elem : Type} -> {nindex : NNat} -> rel nindex NZ -> PreVec elem nindex
    VCons : {elem : Type} -> {nindex : NNat} -> {ntail : NNat} -> elem -> PreVec elem ntail -> rel (NSucc ntail) nindex -> PreVec elem nindex


data PC :  {tipe1 : Type} -> {tipe2 : Type} -> tipe1 -> tipe2 -> Type where
    PCNone : {a : tipe1} -> {b : tipe2} -> PC a b 
    PCCons : {elemType : Type} -> {n1 : NNat} -> {n2 : NNat} -> {nwhole : NNat} ->
            {t1 : PreVec (PC {tipe1 = NNat} {tipe2 = NNat} ) elemType n1} -> 
            {t2 : PreVec (PC {tipe1 = NNat} {tipe2 = NNat} ) elemType n2} ->  
            PC h1 h2 ->
            PC t1 t2 -> 
            (pf1 : PC (NSucc n1) (NSucc nwhole)) -> 
            (pf2: PC (NSucc n2) (NSucc nwhole)) ->
            PC (VCons PC {ntail=n1} {elem=elemType} h1 t1 pf1) (VCons PC {ntail=n2} {elem=elemType} h2 t2 pf2) 


trans : {tx : Type} -> {ty : Type} -> {tz : Type} -> {x : tx} -> {y : ty} -> {z : tz} ->  
     PC x y -> PC y z -> PC x z
trans PCNone pf2 = ?trans_1
trans (PCCons y z pf1 x) pf2 = ?trans_2

标签： functional-programmingpattern-matchingidrisdependent-type

解决方案

首先，大小写分离器相当笨拙，目前独立于类型检查器。它的主要作用是创建每个案例并询问类型检查器该分支是否有效。

我找到了一个显示类似问题的最小示例。

data PreVec : Nat -> Type where
  VCons : PreVec n

data Bad :  {tipe1 : Type} -> tipe1 -> Type where
  MkBad : Bad VCons

data Good1 : PreVec n -> Type where
  MkGood1 : Good1 VCons

data Bad2 : {tipe1: Type} -> tipe1 -> Type where
  MkBad2 : {n: Nat} -> Bad2 (VCons {n})

以类似的方式使用这些会在 Bad 构造函数上产生错误，但会在好的构造函数上找到。

我不能说我完全理解这个问题，但它似乎主要与类型等隐式的解析顺序有关，它可能是一个编译器错误。基本上，隐式tipe1取决于n封装在构造函数本身中的变量。我的猜测是，类型中的隐式在构造函数打开之前被填充，所以这n不在模式类型的范围内。

似乎有多个补丁可以修复它。如果变量tipe1（或tipe2）是显式而不是隐式的，那么使用_无处不在会为您的示例正确合成类型。或者，将返回类型更改为：

PC (the (PreVec elemType (NSucc nwhole)) (VCons PC elemType (NSucc nwhole) n1 h1 pf1))
          (VCons PC elemType (NSucc nwhole) n2 h2 pf2)

也成功了。不成功的一件事是将其他所有隐式更改为显式，它只与这些tipe1和tipe2有关。它们在构造函数中的每个实例都受到约束，因此类型本身没有问题。只有在执行模式匹配时才会出现这种情况。

推荐阅读