Typechecking problem (I'm too dumb for this!)

[Racket Noob]

I don't understand why the following code doesn't  typecheck:

(0-) (tc +)

(datatype tree

  Label : A;

  _________________

  Label : (tree A);

  Label : A; Subtree : (tree A); Subtrees : (list (tree A));

  ===========================================================

  [Label Subtree | Subtrees] : (tree A);

)

(define leaves

  { (tree A) --> (list A) }

  [Label Subtree | Subtrees] -> (append (leaves Subtree)

                                        (leaves* Subtrees))

  Label -> [Label])

(define leaves*

  { (list (tree A)) --> (list A) }

  [] -> []

  [T | Ts] -> (append (leaves T) (leaves* Ts)))

true

(1+) type#tree : symbol

(2+) type error in rule 1 of leaves

(3+) type error in rule 2 of leaves*

(4+) 

What's the problem with the code above?

(I'm so sad because it's gradually become clearer to me that I'm never gonna get a grip with shen type system... :(   )

RacketNoob

[Mark Tarver]

Take your def ....

(define leaves

  {(tree A) --> (list A)}

  [Label Subtree | Subtrees] -> (append (leaves Subtree) (leaves* Subtrees))

  Label -> [Label])

  

The last line requires Shen to prove

  

  Label : (tree A) >> [Label] : (list A)

  

ergo 

  

  Label : (tree A) >> Label : A

  

But your type theory 

(datatype tree

  Label : A;

  _________________

  Label : (tree A);

  Label : A; Subtree : (tree A); Subtrees : (list (tree A));

  ===========================================================

  [Label Subtree | Subtrees] : (tree A);)

only allows

  

   Label : A >> Label : (tree A)

   

So Shen gets stuck!

Back in England in 1 week.

   

Mark

[Mark Thom]

The problem is that, in leaves, the "Label" pattern is a wildcard that could stand for anything, and the type theory as specified can't infer that it's of type A.

Why is that? You've said in the first rule that any value of type A, which you've named Label, is of type (tree A) if it can be shown to be of type A.
This is an introduction form. Note the lack of symmetry: it doesn't follow from this rule alone that if Label is of type (tree A), it is of type A.

Now, we could replace the first sequent rule with

  Label : A;

  =================

  Label : (tree A);

to get that symmetry, but that would be a mistake. That would make *any* tree, including a composite tree with branches,
inferrable as an A, and that's almost certainly not what you want.

One solution is to provide tags to the type checker to ease the distinction between the two cases. Here's what
I have. Notice the use of the non-pattern symbols leaf and tree.

(datatype tree
 
  Leaf : A;
  =======================
  [leaf Leaf] : (tree A);

  Label : A; Subtree : (tree A); Subtrees : (list (tree A));
  ===========================================================

  [tree Label Subtree | Subtrees] : (tree A);)

(define leaves
  { (tree A) --> (list A) }

  [tree Label Subtree | Subtrees] -> (append (leaves Subtree)
                         (leaves* Subtrees))
  [leaf Label] -> [Label])

[Racket Noob]

Thanks to (both) Mark's, now I understand my mistake. :)

But, I'm still wondering if it's possible to give alternative type theory for this problem without introducing tags for leaf and tree ?

Any thoughts?

RacketNoob

[Racket Noob]

Actually I have two more questions about shen typechecking: On the page 236 of TBoS, 2nd edition, there are exercises 19.3 and 19.4. (19.4 is similar to the problem with trees from my last post, while 19.3 asks us about some "!" notation in sequents that I don't understand). Can someone solve those two problems in a way they actually meant to be solved? 

Thanks! 

 

[Mark Thom]

You could get rid of the first sequent rule and keep the second, without need of the 'tree' tag. For an empty tree, you'd add the rule

______________
[] : (tree A);

[fuzzy wozzy]

I don't have a clue what all this is about, but strangely enough "type error in rule 1 of leaves" doesn't appear in windows.

[fuzzy wozzy]

also, just noticed it, but the only error that shows doesn't have an asterisk next to leaves, that is, it appears as,
"type error rule 2 of leaves", too bad type rules don't have to have comments...