Выбор класса типов по строительству типа данных

Question

У меня есть тип данных в Идрисе:

data L3 = Rejected | Unproven | Proven 

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

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

Om [Proven, Unproven, Op [Proven, Oj [Unproven, Proven]] 

Это не реальное представление, я лишен некоторых необходимых уродливых частей, но она дает представление о том, что я пытаюсь достичь, выше эквивалентно:

meet Proven (meet Unproven (Proven <+> (join Unproven Proven))) 

Я узнал, что могу объединить типы данных вместе. Чтобы попасть туда, я создал функцию, которая будет выбрать правильный экземпляр класса:

%case data Operator = Join | Meet | Plus | Mult 

classChoice : (x: Operator) -> (Type -> Type) 
classChoice Join = VerifiedJoinSemilattice 
classChoice Meet = VerifiedMeetSemilattice 
classChoice Plus = VerifiedGroup 
classChoice Mult = VerifiedRing 

Так что я мог бы гарантировать, что все в типе представляет собой один из этих четырех операций:

%elim data LogicSyntacticalCategory : classChoice op a => (op : Operator) -> (a : Type) -> Type where 
     LSCEmpty : LogicSyntacticalCategory op a 

Он пожалуется с :

When elaborating type of logicCategory.LSCEmpty: 
Can't resolve type class classChoice op ty 

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

Код на самом деле не нужен, я вполне доволен направлением мысли.

Answer 1

Две второстепенные проблемы: ... -> a -> ... должен быть ... -> (a : Type) -> ..., а синтаксический - как это написано.

Предупреждение: Я работаю с Idris 0.9.18 и не знаю, как написать Elab proofs.

Repository: https://github.com/runKleisli/idris-classdata

В нормальных функциях с этой же сигнатурой типа, у вас есть возможность помочь разрешению класса типа с тактикой при определении функций. Но с типом данных и его конструкторами у вас есть только возможность объявить их, поэтому у вас нет такой возможности для оказания помощи в разрешении. Казалось бы, такое руководство было необходимо здесь.

Похоже, что classChoice op a нуждается в экземпляре, доказанном до того, как LogicSyntacticleCategory op a в определении LSCEmpty имеет смысл и что он не получил этот экземпляр. Ограничения класса в типе типа данных, подобные этому, обычно автоматически вводятся в контекст конструктора, как неявный аргумент, но это, кажется, не сработало здесь, и экземпляр предполагается для другого типа, чем тот, который требуется. Этот экземпляр, предполагаемый для конструктора, не удовлетворяющего цели, введенной объявлением LogicSyntacticleCategory op a, кажется ошибкой. В одном из примеров в репозитории эти неожиданно несогласованные цели и предположения кажутся способными автоматически спариваться, но не в данных типа данных & объявлений конструктора.Я не могу определить точную проблему, но, похоже, она не применяется к объявлениям с простой функцией с теми же условиями на сигнатуре типа.

пару решений приведены в хранилище, но самый простой заключается в замене ограничения аргумент, говоря, экземпляр classChoice op a требуется, с неявным аргументом типа classChoice op a и оценить LogicSyntacticleCategory как

feat : Type 
feat = ?feat' 

feat' = proof 
    exact (LogicSyntacticleCategory Mult ZZ {P=%instance}) 

Если вы настроены на имеющие ограничения аргумент в вашем главном интерфейсе с типом данных, вы можете обернуть определение LogicSyntacticleCategory : (op : Operator) -> (a : Type) -> {p : classChoice op a} -> Type с функцией

logicSyntacticleCategory : classChoice op a => (op : Operator) -> (a : Type) -> Type 
logicSyntacticleCategory = ?mkLogical 

mkLogical = proof 
    intros 
    exact (LogicSyntacticleCategory op a {P=constrarg}) 

и когда вы хотите, чтобы сделать тип формы LogicSyntacticleCategory op a, оценить, как и раньше, но с

feat' = proof 
    exact (logicSyntacticleCategory Mult ZZ) 
    exact Mult 
    exact ZZ 
    compute 
    exact inst -- for the named instance (inst) of (classChoice Mult ZZ) 

, где последняя строка отбрасывается для анонимных экземпляров.