The Coq mailing list

[Valentin Robert <valentin.robert.42 AT gmail.com>]

Assertion 1 is correct.

Assertion 2 is correct, except maybe the part about next.

Assertion 3 is correct for select, not so much for eta_index.
A safe map would have some sort of (T -> T) as input to transform each
element I guess.
I'm not quite sure what the point of eta_index is to be honest.

- Valentin

On Mon, Aug 12, 2013 at 7:45 PM, t x 
<txrev319 AT gmail.com>
 wrote:
> I was confused due to not understanding the fundamentals. The link was very
> helpful (since the code lacked comments).
>
> Are the following correct?
>
> Assertion 1: so informally,
>   "index n" is a way to encode {x : 0 <= x < n} as
>     None, Some None, Some (Some None), ..., Some^{n-1} None
>
> Assertion 2:
>   first always returns None
>   last n always returns Some^{n-1} None
>   next is meant to build intermediate terms
>   lift is from {x : 0 <= x < n} to {x : 0 <= x < n+1}
>
> Assertion 3:
>   select is "safe nth"
>   eta_index is "safe map"
>
>
>
>
> On Mon, Aug 12, 2013 at 4:56 PM, Valentin Robert
> <valentin.robert.42 AT gmail.com>
>  wrote:
>>
>> 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!
>
>