Re: 3.20 Type Inference

[Jay McCarthy]

That's not in the syntax of the typei language.... so how could you generate constraints for it? What did you find hard about it though?

Jay

On Tue, Nov 29, 2011 at 4:33 PM, mike <neob...@gmail.com> wrote:

hey jay, im having troble denoting constaints given a segment of code. Could you give me a quick example of this to help me understand the process.

{fun {D c1} : c2 (+ 1 D)}

i have been looking in the book but have been unabe to figure out how to apply the method used there to this syntax.


--
The biggest question in my life : How many skittles could fit in an Olympic swimming pool?

--
Jay McCarthy <j...@cs.byu.edu>
Assistant Professor / Brigham Young University
http://faculty.cs.byu.edu/~jay

"The glory of God is Intelligence" - D&C 93

[Jay McCarthy]

Oh, I missed the subject line. So I couldn't tell this was about the written one.

(fun (D : c1) : c2 (+ 1 D))

would have the labeling

[0](fun (D : c1) : c2 [1](+ 1 D))

and the constraints

(from 0)

[0] = D -> [1]

[0] = c1 -> c2

(from 1)

[1] = num

D = num

Jay

On Tue, Nov 29, 2011 at 5:34 PM, mike <neob...@gmail.com> wrote:

I was mimicking the sintax of the language of problem 3.20.2 witch i know is not the typei language. However in said problem you are asking us (the sutdents) to generate constraints from a program in this not typei language. I was asking you to provide an example of how you would do this (generate constraints) from a program in this language (the not typei language).

will you provide such an example?

[mike]

thanks that helps a lot!

[Erik Donohoo]

JAY!
We can't figure out the constraints. I feel like if you will show us
what the constraints would be on these examples, how they are
"labeled" and so forth, that we will understand how to write the
generate constraints method

(bin-num-op + (num4) (num 5))
(with ('x (num 5)) (bin-num-op + (with ('y (num 4)) (bop + (num 3) y))
(id 'x)))

How do you know whether to label the insides of a bin-num-op?

On Nov 30, 2:55 pm, mike <neobob...@gmail.com> wrote:
> thanks that helps a lot!
>
>
>
>
>
>
>
>
>
> On Tue, Nov 29, 2011 at 6:45 PM, Jay McCarthy <j...@cs.byu.edu> wrote:
> > Oh, I missed the subject line. So I couldn't tell this was about the
> > written one.
>
> > (fun (D : c1) : c2 (+ 1 D))
>
> > would have the labeling
>
> > [0](fun (D : c1) : c2 [1](+ 1 D))
>
> > and the constraints
>
> > (from 0)
> > [0] = D -> [1]
> > [0] = c1 -> c2
>
> > (from 1)
> > [1] = num
> > D = num
>
> > Jay
>

> > On Tue, Nov 29, 2011 at 5:34 PM, mike <neobob...@gmail.com> wrote:
>
> >> I was mimicking the sintax of the language of problem 3.20.2 witch i know
> >> is not the typei language. However in said problem you are asking us (the
> >> sutdents) to generate constraints from a program in this not typei
> >> language. I was asking you to provide an example of how you would do this
> >> (generate constraints) from a program in this language (the not typei
> >> language).
>
> >> will you provide such an example?
>
> >> On Tue, Nov 29, 2011 at 5:03 PM, Jay McCarthy <j...@cs.byu.edu> wrote:
>
> >>> That's not in the syntax of the typei language.... so how could you
> >>> generate constraints for it? What did you find hard about it though?
>
> >>> Jay
>

[Erik Donohoo]

To further clarify, if i labeled as follows:

[0](binnumop + (num 4) (num 5))

I would get
[0] = num num -> num right?
are there any other labels necessary here?

[Jay McCarthy]

[0](+ [1]4 [2]5)

with

0

[0] = num

[1] = num

[2] = num

1

[1] = num

2

[2] = num

[Jay McCarthy]

You label every expression. You should look at the table in Chapter 30.

[Wayne Robison]

Jay,

In class, you generated constraints for binary operations (like * and +) like this:

Expression:

[0](* n [1](+ 4 5))

Constraints Generated from [0]:

* = n [1] -> [0]

* = num num -> num

When we unified these, we got the contraints

n = num

[1] = num

[0] = num

In the table in the book, and how we're doing it in the assignment, it seems we're skipping the first two constraints and going straight to the second set of three constraints.  I'm assuming that this is correct, but wanted to make sure we weren't missing something.

It seems to me like we can't make constraints of the former type anyway, since they have two arguments.

Another question relating to labeling list types:

When we're looking at a first, we know that the expression has to be of type list, but a list has a type of what is inside it as well, right?  And so we need to label that type so that we can constrain it to be the return type of the first expression.  A similar problem comes up with rest.  How would we write the constraint for a list type?  Do we just give it some random label like we do in the implementation?

Thanks,

--Wayne

[Jay McCarthy]

On Thu, Dec 1, 2011 at 11:42 AM, Wayne Robison <reallybla...@gmail.com> wrote:

Jay,

In class, you generated constraints for binary operations (like * and +) like this:

Expression:

[0](* n [1](+ 4 5))

Constraints Generated from [0]:

* = n [1] -> [0]

* = num num -> num

When we unified these, we got the contraints

n = num

[1] = num

[0] = num

In the table in the book, and how we're doing it in the assignment, it seems we're skipping the first two constraints and going straight to the second set of three constraints.  I'm assuming that this is correct, but wanted to make sure we weren't missing something.

Yup, I just think it is more confusing to have duplicated function application logic.

 

It seems to me like we can't make constraints of the former type anyway, since they have two arguments.

Another question relating to labeling list types:

When we're looking at a first, we know that the expression has to be of type list, but a list has a type of what is inside it as well, right?  And so we need to label that type so that we can constrain it to be the return type of the first expression.  

Yup

 

A similar problem comes up with rest.  How would we write the constraint for a list type?  Do we just give it some random label like we do in the implementation?

Yup

Jay

 

Thanks,

--Wayne