Choosing a typeclass on construction of a data type

Question

I have a a data type in idris:

data L3 = Rejected | Unproven | Proven

which I verified to be a ring with unity, a lattice, a group and some other properties too.

Now I want to create an object, which preserves the expressions of the statements I inject in it. I started out with four categories to represent all the operations, so I get a nice syntax tree out of it. Eg:

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

This is not the real representation, I stripped some of the needed ugly parts, but it gives an idea of what I try to achieve, the above is equivalent to:

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

I recognized I could join the data types together into one. To get there I created a function, which will pick the correct class instance:

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

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

So I could assure that anything in the type represents one of those four operations:

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

It will complain with:

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

Now my question: How can I assure that the objects in my data type are verified and join the four separate data types into one. I really would like to ensure this is true during construction. I can understand it has difficulties resolving the type class now, but I want Idris to ensure it can do it later during construction. How can I do this?

Code isn't really needed, I am quite happy with a direction of thought.

runKleisli runKleisli · Accepted Answer · 2016-02-21T18:37:04

Two minor problems first: ... -> a -> ... should be ... -> (a : Type) -> ..., and syntactical is how it's written.

Warning: I'm working with Idris 0.9.18 and don't know how to write Elab proofs yet.

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

In normal functions with these same type signatures, you have the opportunity to assist the type class resolution with tactics while defining the functions. But with the data type and its constructors, you only have the opportunity to declare them, so you have no such opportunity to assist in resolution. It would appear such guided resolution was needed here.

It appears that classChoice op a needs an instance proved before the LogicSyntacticleCategory op a in the definition of LSCEmpty makes sense, and that it did not get this instance. Class constraints in the data type's type like this are usually automatically introduced into the context of the constructor, like an implicit argument, but this seems to have failed here, and an instance is assumed for a different type than the one required. That instance assumed for the constructor not satisfying the goal introduced by declaring a LogicSyntacticleCategory op a seems to be the error. In one of the examples in the repository, these unexpectedly mismatched goal and assumption seem able to automatically pair, but not under the circumstances of the data type & constructor declarations. I can't figure out the exact problem, but it seems not to apply to plain function declarations with the same conditions on the type signature.

A couple solutions are given in the repository, but the easiest one is to replace the constraint argument, saying an instance of classChoice op a is required, with an implicit argument of type classChoice op a, and to evaluate LogicSyntacticleCategory like

feat : Type
feat = ?feat'

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

If you are set on having a constraint argument in your main interface to the data type, you can wrap the definition of LogicSyntacticleCategory : (op : Operator) -> (a : Type) -> {p : classChoice op a} -> Type with the function

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

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

and when you want to make a type of the form LogicSyntacticleCategory op a, evaluate like before, but with

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

where the last line is dropped for anonymous instances.

Choosing a typeclass on construction of a data type

1 Answers