Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] ltamer/src/coq/Util.v : intuition of "tuple"

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] ltamer/src/coq/Util.v : intuition of "tuple"


Chronological Thread 
  • From: Valentin Robert <valentin.robert.42 AT gmail.com>
  • To: t x <txrev319 AT gmail.com>
  • Cc: coq-club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] ltamer/src/coq/Util.v : intuition of "tuple"
  • Date: Mon, 12 Aug 2013 17:56:28 +0100

Hmmm, I don't think there's much to point you at.

Maybe you will want to take a look at the paragraph "Recursive Type
Definitions" in this chapter of CPDT:
http://adam.chlipala.net/cpdt/html/DataStruct.html

This is a fixpoint encoding of homogeneous nested tuples (repeat) and
of finite natural numbers (index).
The latters allow you to safely index a position inside the formers.

The functions are then defined in a somewhat straightforward way:

first is a safe zero.
next is a safe successor function.
last builds (n - 1), the biggest safe index in a set of n elements.
lift lifts an index in a bigger set: it has the same value, but
indexes a set with an additional element.
select safely retrieves an element from a tuple.
eta_index is just some sort of eta-expansion for safely-indexed
collections apparently.

What is confusing you? Is it how these typecheck, what they define, or
the reason why they are defined this way? Or something else?

- Valentin

On Mon, Aug 12, 2013 at 5:36 PM, t x
<txrev319 AT gmail.com>
wrote:
> In the lambda tamer source, /src/coq/Util.v, there's the following block of
> code:
>
> https://gist.github.com/anonymous/76f36130b1bb9a2f6786
>
> I've played around with a few "Eval compute in ... "
>
> however, it's not clear to me what the intuitive definitions for:
> "first, next, last, lift, select, eta_index"
> are.
>
> Can someone point me at a paper/reference on the theoretical model behind
> this "tuple" ?
>
> Thanks!



Archive powered by MHonArc 2.6.18.

Top of Page