8
$\begingroup$

Record types are a common feature in most paradigms. Agda also allows defining records with the coinductive keyword. Lastly there are the seemingly more exotic co(inductive)data types which are kind of the duals of inductive types, in the sense that they're defined by projections rather than constructors.

What are the differences between all of these? Is one more powerful than the rest?

$\endgroup$

1 Answer 1

4
$\begingroup$

By reading your question, I believe that you are not looking for a very technical answer, but general ideas instead. If you would like to dig deeper, you can search with the keyword 'polarity' and 'later modality'.

I would say in Agda, coinductive records is a technique of implementing codata types. There are others, such as the Coq CoInductive and the Agda's old musical notations, and I believe they're all different ways to express the so-called "codatatypes". There is a subtle difference between coinductive records and Coq CoInductive, which I do not want to explain here.

Records in Agda are by default non-recursive, say, you may think of them as a named version of sigma types (so they have η-rules, etc.), but coinductive records are totally different, either in the semantic sense or in the typing rules of type theory. They have a special termination checker (the "productivity checker") and allows negativity. So, I would say, the two features look similar is only because the information you provide to define a record & a coinductive type is similar -- parameters, the universe it lives in, and a list of types with names which are fields for records and projections/copatterns for coinductive records.

I think the similarity is also due to the fact that sigma types is positive and negative at the same time (there are equivalent ways to define it, one positive and one negative), but still coinductive records are more complicated than negative sigma types.

$\endgroup$
7
  • 2
    $\begingroup$ I wouldn't call record types in Agda/Coq style "inductive types", though. Because they have η rules and are primitively handled through projections, they feel very negative to me, so I would rather understand them as non-recursive coinductive type. Although they are nice and simple because they do not have the complicated infinitary behaviour of general coinductive types. $\endgroup$ Dec 2, 2022 at 10:16
  • $\begingroup$ @MevenLennon-Bertrand I agree. Changed the wording. $\endgroup$
    – ice1000
    Dec 2, 2022 at 15:15
  • 3
    $\begingroup$ It would be helpful to define "coinductive", "codata", and "negative". I don't know of such a definition myself, but "non-recursive coinductive" sounds like an oxymoron to me, or is the notion of (co)induction not necessarily entangled with recursion? $\endgroup$
    – Li-yao Xia
    Dec 2, 2022 at 16:16
  • 2
    $\begingroup$ @Li-yaoXia function types would be an example where (co)induction isn't connected with recursion exactly. IMO it is clearer to (equivalently) rephrase things in terms of recursors and eta laws (such as extensionality for functions.) $\endgroup$ Dec 2, 2022 at 17:27
  • 1
    $\begingroup$ As for the other two, I am not sure what the difference between coinductive and codata is. In both cases, I would say this corresponds categorically to greatest fixpoints of (polynomial) functors (while inductive types are smallest fixpoints), and the translation of these into (dependent) type theory. The difficulty is that there are different such translations: Coq's old "positive" presentation mimicking the syntax for inductives, Agda's musical notations, co-inductive records, co-patterns… AFAICT, the (soft) question of which is the best approach to manipulate coinduction is still open. $\endgroup$ Dec 3, 2022 at 12:55

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.