Generic programming again, now exercise 3.

[Serguey Zefirov]

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)
------------------------------------------------------------------------------

[peter morris-2]

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 <sergueyz@...> 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)
------------------------------------------------------------------------------

[Serguey Zefirov]

> 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 :)

I found some errors you mentioned by myself and I stopped reading with
attention when I realized that I am on the right track (yes, wNil with
parameter). Now it took me more than several seconds after the sending
mail here. ;)

I haven't had time to verify my thoughts yet but I think I know how to
do it right.