6
$\begingroup$

If we have univalence at hand, the records and iterated sigma versions of some type will be equal. Still, there may be some important typechecking-related differences.

For example, it seems that one could control eta-equality more finely by mixing usages of a no-eta-sigma with a with-eta-sigma (I could be totally wrong). I've also heard that records are "injective" and that they let the typechecker infer types more easily, though I don't really understand what is meant by this (a clarification of this would also be appreciated).

What other differences for typechecking are there? (This question is restricted to those records that can be expressed using iterated sigmas)

$\endgroup$
4
  • 1
    $\begingroup$ If I am to say anything, it will be mainly related to user experience and convenience. Is that the kind of answers you're looking for? $\endgroup$
    – ice1000
    Commented Apr 30 at 20:35
  • $\begingroup$ It depends I guess. I know that stuff like using modules an instantiation only can be done with records, but I'm thinking if somehow agda can infer differently in both context. So more in the way of convinience focused on type checking, i.e. specifying signature and omitting types in definitions (i.e. type inference). $\endgroup$ Commented May 1 at 19:58
  • 2
    $\begingroup$ I'll try to give a proper answer over the weekend, but the main difference is indeed that record type constructors are injective with respect to definitional equality in all parameters, whereas a function mapping into iterated sigma-types need not be. $\endgroup$
    – James Wood
    Commented May 3 at 7:18
  • $\begingroup$ @JamesWood I'll be waiting for it! $\endgroup$ Commented May 3 at 17:16

1 Answer 1

1
$\begingroup$

There is no typechecking difference because Sigma types are records in Agda.

So generally, Sigma types represent a subset of the options one has for declaring record types (eta or no, inductive or no, etc.) But it's records, not sigmas, that are the primitive feature in Agda.

$\endgroup$
1
  • 2
    $\begingroup$ I think the question is about comparing using a single record to iterated sigma-types. These do behave differently for equivalent types. $\endgroup$
    – James Wood
    Commented May 3 at 7:15

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.