Hi Serguey,
> When I meditated on that exercise I come to interesting conclusion.
> wNat has a "type" *, and has a value from "universe of types", W Bool
> So. Does it mean that when we declare wZero : wNat, wNat gets
> "expanded" and its' value gets substituted as the type for wZero?
No, the definition wNat contains representatives for all Natural Numbers
regardless of the definitions wZero and wSuc. The point of defining these
'constructors' is simply to equip this generic encoding of Nat with the
standard, Peano interface (at least when it comes to constructing natural
numbers, elimination is another matter). They do not change the fact that
wNat is already closed under zero and successor.
> My description of Lists follows wNat example from paper. Did I
> described Lists correctly?
Given that the 'constructors' wZero and 'wSuc' do not "expand" the
definition of wNat the definition of 'wList' must be different from that of
'wNat'. You should be suspicious that the element 'a : A' appears nowhere on
the right-hand side of your definition of 'wCons'. (Also I worry that your
wNil constructor also takes an element of 'A', surely the empty list
contains no 'A's?). Generally the 'S' in 'W S P' must contain information
about the type's constructors *and* non-recursive arguments. You use 'Bool'
for 'S' in the definition of 'wNat' though one could define a new type with
more informative constructor names:
data NatCons : * where nczero : NatCons ; ncsuc : NatCons
The 'P' part then defines how many recursive arguments each constructor
takes, 'Oh' dictates that 'false' (or 'nczero') has none, and 'true'
('ncsuc') has one. While the definition of 'wList' has a similar shape to
'wNat' one must account in the definition for the presence of an 'A' in the
constructor 'wCons'.
I've tried not to give away to much so that you can complete the exercise
yourself, but I fear this may have caused me to be less than clear in
places. If you find you are still lost, please don't hesite to ask more
questions :)
Peter
On 26/02/2008, Serguey Zefirov <[EMAIL PROTECTED]> wrote:
>
> I decided to start from something lighter than BTree. I choosed a
> List. This is easy because Lists are very like Nats, just a little bit
> more polymorphic.
>
> When I meditated on that exercise I come to interesting conclusion.
> wNat has a "type" *, and has a value from "universe of types", W Bool
> So. Does it mean that when we declare wZero : wNat, wNat gets
> "expanded" and its' value gets substituted as the type for wZero?
>
> My description of Lists follows wNat example from paper. Did I
> described Lists correctly?
>
>
> ------------------------------------------------------------------------------
> let (----------!
> ! wNat : * )
>
> wNat => W Bool So
>
> ------------------------------------------------------------------------------
> let (--------------!
> ! wZero : wNat )
>
> wZero => Sup false notSo
>
> ------------------------------------------------------------------------------
> ( n : wNat !
> let !---------------!
> ! wSuc n : wNat )
>
> wSuc n => Sup true (lam p => n)
>
> ------------------------------------------------------------------------------
> ( A : * ; a : A !
> let !----------------!
> ! wList a : * )
>
> wList a => W Bool So
>
> ------------------------------------------------------------------------------
> ( a : A !
> let !------------------!
> ! wNil a : wList a )
>
> wNil a => Sup false notSo
>
> ------------------------------------------------------------------------------
> ( a : A ; as : wList A !
> let !-----------------------!
> ! wCons a as : wList A )
>
> wCons a as => Sup true (lam p => as)
>
> ------------------------------------------------------------------------------
>
