Выражение регистра в зависимом типе не работает должным образом в Idris - PullRequest
Новая
       11

Выражение регистра в зависимом типе не работает должным образом в Idris

0 голосов
/ 08 февраля 2019

Я портирую небольшие порции кода PureScript на Idris, где зависимые типы могут применяться и сталкиваться с ситуацией, когда использование case внутри зависимого типа не работает.

Так как это действительно (упрощенно): 

data ValidInvoice3 : (ft : FeeType) -> Type where
  MkVI3 : ValidInvoice3 ft

почему следующее не проверяет тип? 

-- BROKEN
data ValidInvoice4 : (ft : FeeType) -> Type where
  MkVI4 : case ft of
            FeeMarkupHidden => ValidInvoice4 ft -- simplified;
            FeeExplicit     => ValidInvoice4 ft -- more elaborate example below

Если вам интересно, почему я смотрю на это: вот немного более сложный пример кода: 

module DependentWithCase

data FeeType = FeeMarkupHidden | FeeExplicit

data Fee : (ft : FeeType) -> Type where
  MkFee : Fee ft -- simplified

data ValidArticle : (ft : FeeType) -> Type where
  MkVA : ValidArticle ft -- simplified

Вот теперь, как можно успешно написать зависимый тип для «счета-фактуры», индексировать его по типу FeeType, используя выражение case, чтобы решить, будет ли плата добавлена ​​как явный параметр (в фактическом кодев этом случае тип «article» имеет часть «разметки», которую я здесь оставил, поэтому я могу быть уверен, что «разметка» выставляется только один раз): 

data ValidInvoice : (ft : FeeType) -> Type where
  MkVI : ValidArticle ft ->
         case ft of FeeMarkupHidden => Unit; FeeExplicit => Fee ft;
         ->
         ValidInvoice ft

Таким образом, вы видите, что тип данных счета-фактуры (и в фактическом коде, тип статьи тоже) зависит от типа платы.

Но вместо использования выражения case, скрытого внутри конструкцииctor, я бы предпочел, чтобы он выглядел как синоним этого типа (который, конечно, не имеет конструктора;но это, по сути, то, как это читается в коде PureScript, но вместо этого используется тип суммы с отдельными конструкторами вместо зависимого типа, индексируемого через FeeType).Это намного более читабельно для меня (особенно в реальном коде). 

ValidInvoice2 : (ft : FeeType) -> Type
ValidInvoice2 FeeMarkupHidden = ValidArticle FeeMarkupHidden -> Unit            -> ValidInvoice2 FeeMarkupHidden
ValidInvoice2 FeeExplicit     = ValidArticle FeeExplicit     -> Fee FeeExplicit -> ValidInvoice2 FeeExplicit

Так почему ValidInvoice4 не проверяет тип?Я пишу это неправильно?Или ожидаете, что что-то сработает, что просто не может работать?

1 Ответ

0 голосов
/ 08 февраля 2019

Похоже, что Идрис не замечает, что любая ветвь вашего заявления о ситуации приводит к ValidInvoice4.Он также не оценивает функции в аналогичной позиции.Вы почти всегда можете сделать что-то немного другое и получить тот же результат.

Глядя на то, что вы пытаетесь достичь, я бы рекомендовал сделать Fee FeeType -индексированный Maybe - что упрощаетвсе дело: 

data FeeType = FeeMarkupHidden | FeeExplicit

data Fee : (ft : FeeType) -> Type where
    HidFee : Fee FeeMarkupHidden
    ExFee : Nat {- or w/e -} -> Fee FeeExplicit

data ValidArticle : (ft : FeeType) -> Type where
    MkVA : ValidArticle ft

data ValidInvoice : (ft : FeeType) -> Type where
  MkVI : ValidArticle ft -> Fee ft -> ValidInvoice ft
...