tBoS p. 229

[unhan...@gmail.com]

There's obviously something about the type checker that I badly misunderstand.  On page 229 you give a first attempt at defining arith-expr, which includes

X:number
__________________
X:arith-expr

I would have thought this allows the type-checker to infer that any number is also an arith-expr.  But you say in the next paragraph that this fails because "+ produces numbers and not arith-exprs as required by our type assignment."  Why is the type-checker unable to make the necessary inference?

[Mark Tarver]

Try using spy - this helps to understand the reasoning.

?- (define do-calculation { arith-expr --> arith-expr } 

         [X + Y] -> (+ (do-calculation X) (do-calculation Y))

         [X - Y] -> (- (do-calculation X) (do-calculation Y))

         [X * Y] -> (* (do-calculation X) (do-calculation Y))

         [X / Y] -> (/ (do-calculation X) (do-calculation Y)) 

         X -> X) : Var2

The first steps establish the integrity condition - that the structure of the input conforms to the type definition for arith-exprs.

____________________________________________________________ 24 inferences

?- [&&X + &&Y] : arith-expr

1. &&X : Var10

2. &&Y : Var13

3. do-calculation : (arith-expr --> arith-expr)

>

____________________________________________________________ 43 inferences

?- [&&X + &&Y] : number

1. &&X : Var10

2. &&Y : Var13

3. do-calculation : (arith-expr --> arith-expr)

>

____________________________________________________________ 68 inferences

?- &&X : arith-expr

1. &&X : Var10

2. &&Y : Var13

3. do-calculation : (arith-expr --> arith-expr)

>

____________________________________________________________ 75 inferences

?- &&Y : arith-expr

1. &&X : arith-expr

2. &&Y : Var13

3. do-calculation : (arith-expr --> arith-expr)

>

This concludes the integrity test; so far so good. Shen now tries to prove that the result has the expected type assuming that the input(s) conform(s) to the type(s) allotted to them.

____________________________________________________________ 86 inferences

?- ((+ (do-calculation &&X)) (do-calculation &&Y)) : arith-expr

1. [&&X + &&Y] : arith-expr

2. do-calculation : (arith-expr --> arith-expr)

This first attempt fails because + does not output arith-expr.

>____________________________________________________________ 95 inferences

?- (+ (do-calculation &&X)) : (Var46 --> arith-expr)

1. [&&X + &&Y] : arith-expr

2. do-calculation : (arith-expr --> arith-expr)

>

____________________________________________________________ 104 inferences

?- + : (Var48 --> (Var46 --> arith-expr))

1. [&&X + &&Y] : arith-expr

2. do-calculation : (arith-expr --> arith-expr)

>

____________________________________________________________ 122 inferences

?- + : (Var48 --> (Var46 --> arith-expr))

1. &&X : arith-expr

2. &&Y : arith-expr

3. do-calculation : (arith-expr --> arith-expr)

>

____________________________________________________________ 156 inferences

?- (+ (do-calculation &&X)) : (Var46 --> arith-expr)

1. &&X : arith-expr

2. &&Y : arith-expr

3. do-calculation : (arith-expr --> arith-expr)

>

____________________________________________________________ 167 inferences

?- + : (Var92 --> (Var46 --> arith-expr))

1. &&X : arith-expr

2. &&Y : arith-expr

3. do-calculation : (arith-expr --> arith-expr)

>

At this point Shen gives up and tries the first rule that you cite.  Prove that an arith-expr is delivered because a number is delivered.

____________________________________________________________ 211 inferences

?- ((+ (do-calculation &&X)) (do-calculation &&Y)) : number

1. [&&X + &&Y] : arith-expr

2. do-calculation : (arith-expr --> arith-expr)

>

____________________________________________________________ 221 inferences

?- (+ (do-calculation &&X)) : (Var136 --> number)

1. [&&X + &&Y] : arith-expr

2. do-calculation : (arith-expr --> arith-expr)

>

____________________________________________________________ 230 inferences

?- + : (Var138 --> (Var136 --> number))

1. [&&X + &&Y] : arith-expr

2. do-calculation : (arith-expr --> arith-expr)

>

Going well; but now we hit the snag - we have to show do-calculation itself produces a number.  Shen cannot prove that because do-calculation produces an arith-expr.  The type checker wanders fruitlessly trying different ways to prove that conclusion before exhausting all possibilities. 

____________________________________________________________ 233 inferences

?- (do-calculation &&X) : number

1. [&&X + &&Y] : arith-expr

2. do-calculation : (arith-expr --> arith-expr)

>

____________________________________________________________ 243 inferences

?- do-calculation : (Var141 --> number)

1. [&&X + &&Y] : arith-expr

2. do-calculation : (arith-expr --> arith-expr)

>

...............................

type error in rule 1 of do-calculation

[unhan...@gmail.com]

Thanks, I didn't know about spy.  I don't understand all the output, but enough to see why the type-checking fails.

Shen is generally an extremely elegant language, but the solution given on p. 231 looks a tad kludgy. It seems like a multiple-dispatch model might be nicer, where one could write

X:number->X

i.e. incorporate the type into the pattern matching.    Is that a model you've purposefully avoided?

[Mark Tarver]

Well, your solution is sort of what is on p 231.  What you have got is a check that X is really a number.  The question is what sort of check is that?  Is it a run-time check - then its equivalent to a verified type.   If it is a compile-time only, you need to ask 'How does this work?'.   

Mark

--
You received this message because you are subscribed to the Google Groups "Shen" group.
To unsubscribe from this group and stop receiving emails from it, send an email to qilang+unsubscribe@googlegroups.com.
To post to this group, send email to qil...@googlegroups.com.
Visit this group at https://groups.google.com/group/qilang.
For more options, visit https://groups.google.com/d/optout.

[unhan...@gmail.com]

Isn't your intention to do compile-time type checking?  In this case we haven't run the function, just defined it.

[Mark Tarver]

Verified types allow you to use run-time processes to garner type information.  If you want to dispense with them here; you need to tag the numbers in your SC definition of arith-expr.

Mark

On Wed, Jun 14, 2017 at 10:44 PM, dabr...@indiana.edu <unhan...@gmail.com> wrote:

Isn't your intention to do compile-time type checking?  In this case we haven't run the function, just defined it.

--

[unhan...@gmail.com]

But in this case you're just defining the function, not running it.  Doesn't that mean that you're using verified for compile-time type checking?

Perhaps what I really mean is that allowing types in the pattern matching would be a good syntactic sugar.  It works nicely in Mathematica.