Можно ли избежать явного сброса недопустимых дел в полных функциях в Idris? - PullRequest
Новая
       66

Можно ли избежать явного сброса недопустимых дел в полных функциях в Idris?

0 голосов
/ 21 марта 2020

Рассмотрим следующий (очень упрощенный) пример ограничения типа данных с помощью побочного условия на его значениях: 

data Transport = Car | Foot | Boat

total wheels : (transport : Transport) -> {auto hasWheels : transport = Car} -> Int
wheels Car {hasWheels = Refl} = 4
wheels Foot {hasWheels = Refl} impossible
wheels Boat {hasWheels = Refl} impossible

Можно ли как-то опустить или суммировать случаи impossible и до сих пор Идрис видит функцию как полную? Если я пропущу кейс, то получу что-то вроде 

Main.wheels is not total as there are missing cases

, я также не смогу просто получить универсальный кейс, так как компилятор не знает, что _ не может быть Car, поэтому вторая строка не проверяет тип: 

wheels Car {hasWheels = Refl} = 4
wheels _ {hasWheels = Refl} impossible

Это дает 

wheels _ is a valid case

Я рассмотрел идеи в этом посте об ограничении типов данных , но Я не вижу подходов, которые бы помогли.

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

1 Ответ

1 голос
/ 25 марта 2020

Я более внимательно изучил подходы, обсуждаемые в вопросе , который я уже связал , и некоторые из них действительно позволяют полностью исключать случаи.

Я придумал следующее, которое кажется лучше всего подходит для моего реального случая использования, когда реальные условия более сложны: 

isCar : Transport -> Bool
isCar Car = True
isCar _ = False

BoolToType : Bool -> Type
BoolToType True = ()
BoolToType False = Void

total wheels
   : (transport : Transport)
  -> {auto hasWheels : BoolToType (isCar transport)}
  -> Int
wheels Car = 4

Однако я не очень понимаю, почему Идрис с удовольствием опускает невозможные шаблоны здесь, но не в моем исходном коде, поэтому ответ, который действительно объясняет, что происходит, все равно будет очень полезен.

...