«Недоступная переменная шаблона» в Идрисе - PullRequest
Новая
       39

«Недоступная переменная шаблона» в Идрисе

1 голос
/ 21 октября 2019

У меня возникла проблема, когда сопоставление с образцом в Idris приводит к ошибкам «недоступная переменная образца», даже когда я просто использую компилятор для управления сопоставлением с образцом.

Вот примерчто я пытаюсь сделатьСпецифика не так уж важна, главное, что у меня есть нечто похожее на вектор, за исключением того, что оно параметризовано по отношению между векторными индексами вместо использования равенства. Затем я получил другой тип, который определяет отношение, где один вариант - это отношение ПК между векторами. (В моем реальном коде есть другие случаи, я только что их исключил).

Затем я пытаюсь определить функцию "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

1 Ответ

1 голос
/ 01 ноября 2019

Прежде всего, разделитель кейсов довольно тупой и не зависит от проверки типов в данный момент. Прежде всего, он создает каждое дело и спрашивает, проверяет ли ветка типов, допустима ли эта ветвь.

Я нашел минимальный пример, который показывает похожие проблемы. 

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})

Использование их в аналогичнойway выдаст ошибки на плохих конструкторах, но нахожу на хороших.

Не могу сказать, что полностью понимаю проблему, но, похоже, это в основном связано с порядком разрешения для таких имплицитов, как типы, это, вероятно, ошибка компилятора. По сути, неявное значение 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. Каждый их экземпляр в конструкторах ограничен, поэтому нет проблем с самим типом. Такая ситуация возникает только при сопоставлении с образцом.

...