typei - tempty

[Stephen Rollins]

I'm trying to write the constraints for tempty, but I don't know what type to give it. We have the t-list type, but it needs to be given another type. What is the type of tempty?

[Jay McCarthy]

You're not sure yet. So you should make a new type that doesn't have
any other constraints on it.

> --
> You received this message because you are subscribed to the Google Groups
> "byu-cs-330-fall-2013" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to byu-cs-330-fall-...@googlegroups.com.
> For more options, visit https://groups.google.com/groups/opt_out.



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

[Stephen Rollins]

What are the implications of this when it comes to the unifying function? I understand that in some cases tempty can be inferred to be of a particular list type (e.g. in '(tcons 1 tempty), it would be coerced into being a list of t-num to satisfy the type inferrer), but what would the type of 'tempty be? Just t-tempty?

What type should be inferred for a program like '(tfirst tempty)? What about '(trest tempty)? Should both of those throw a type error? If so, at what point would we finally declare that a type error has indeed been found? What if we had a program like '(+ 1 (tfirst tempty))? Would tempty be inferred to be a list of t-num and a type error not be thrown?

[Jay McCarthy]

On Tue, Nov 26, 2013 at 6:32 PM, Stephen Rollins
<enzed....@gmail.com> wrote:
> What are the implications of this when it comes to the unifying function?

I can't write the function for you.

> I
> understand that in some cases tempty can be inferred to be of a particular
> list type (e.g. in '(tcons 1 tempty), it would be coerced into being a list
> of t-num to satisfy the type inferrer), but what would the type of 'tempty
> be? Just t-tempty?

t-empty is not a type. It has to be t-list of something.

>
> What type should be inferred for a program like '(tfirst tempty)? What about
> '(trest tempty)?

The whole point of type inference is that these questions cannot be
answered without respect the rest of the program.

> Should both of those throw a type error?

What is the constraint that is too tight that makes you think there's

a type error?

> If so, at what
> point would we finally declare that a type error has indeed been found? What
> if we had a program like '(+ 1 (tfirst tempty))? Would tempty be inferred to
> be a list of t-num and a type error not be thrown?

Why would you think that?

Jay

[Stephen Rollins]

When I first asked you about the type of tempty, you said

"You're not sure yet. So you should make a new type that doesn't have any other constraints on it."

I understand that this new type is not really a type, but merely a filler that should be handled at a later time. My confusion partly comes from what to do with this "filler" tempty type in the meantime. I know that the hope is to eventually discern what type of list we need in place of this filler tempty type, but what happens if we have a program that never provides enough context to decide what type of list we needed? That's what I meant when I asked about programs like '(tfirst tempty).

I can understand conceptually what functions would do in this case. For example, if we have '(fun (x) x), then we have a program that is of type (t-fun (t-val 'x) (t-val 'x)). However, given more context, we might be able to infer the type of this function, such as in a program like '(+ 1 ((fun (x) x) 2)), where we would infer the function's type to be (t-fun (t-num t-num)). I'm confused how to apply this concept to empty lists. If I had the program '(tcons 1 tempty), then naturally tempty would be inferred as type (t-list (t-num)). But what if I didn't have enough context to interpret what type of list tempty was? If functions don't have enough context, we can use the t-val type. What can we do for empty lists that lack sufficient context to infer their type?

[Jay McCarthy]

Why do you think you need to "do" anything? If a program is
under-constrained, then it will end up with type variables that don't
get constrained to be anything, which means it is polymorphic. Thus,
it is incorrect in general to think that every type variable must be
"filled in". In any case, there's nothing you could do in the tempty
constraints to make it filled it... that's a result of the unification
process.

Jay

On Tue, Nov 26, 2013 at 8:16 PM, Stephen Rollins

[Stephen Rollins]

Maybe that's my real question, then: how to represent a polymorphic list. And I think I am talking more about the unification process now rather than just constraint generation. But, ultimately, when we run infer-type on a program, we need to return the type said program, yes? So what would the type be for an empty list? Obviously the program '(trest (tcons 1 tempty)) would have the type (t-list (t-num)). But what about the program 'tempty?

[Jay McCarthy]

I've already told you. "You should make a new type [variable] that

doesn't have any other constraints on it."

On Tue, Nov 26, 2013 at 9:23 PM, Stephen Rollins

[Scott Heidbrink]

So is that like the [tExpr (e : ExprC)] type in the book?

>> >> >> > email to byu-cs-330-fall-2013+unsub...@googlegroups.com.

>> >> >> > For more options, visit https://groups.google.com/groups/opt_out.
>> >> >>
>> >> >>
>> >> >>
>> >> >> --
>> >> >> 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
>> >> >
>> >> >
>> >> > --
>> >> > You received this message because you are subscribed to the Google
>> >> > Groups
>> >> > "byu-cs-330-fall-2013" group.
>> >> > To unsubscribe from this group and stop receiving emails from it,
>> >> > send
>> >> > an

>> >> > email to byu-cs-330-fall-2013+unsub...@googlegroups.com.

>> >> > For more options, visit https://groups.google.com/groups/opt_out.
>> >>
>> >>
>> >>
>> >> --
>> >> 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
>> >
>> >
>> > --
>> > You received this message because you are subscribed to the Google
>> > Groups
>> > "byu-cs-330-fall-2013" group.
>> > To unsubscribe from this group and stop receiving emails from it, send
>> > an

>> > email to byu-cs-330-fall-2013+unsub...@googlegroups.com.

>> > For more options, visit https://groups.google.com/groups/opt_out.
>>
>>
>>
>> --
>> 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
>
>
> --
> You received this message because you are subscribed to the Google Groups
> "byu-cs-330-fall-2013" group.
> To unsubscribe from this group and stop receiving emails from it, send an

> email to byu-cs-330-fall-2013+unsub...@googlegroups.com.

[Jay McCarthy]

Yup

Sent from my iPhone

>> >> >> > email to byu-cs-330-fall-...@googlegroups.com.

>> >> >> > For more options, visit https://groups.google.com/groups/opt_out.
>> >> >>
>> >> >>
>> >> >>
>> >> >> --
>> >> >> 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
>> >> >
>> >> >
>> >> > --
>> >> > You received this message because you are subscribed to the Google
>> >> > Groups
>> >> > "byu-cs-330-fall-2013" group.
>> >> > To unsubscribe from this group and stop receiving emails from it,
>> >> > send
>> >> > an

>> >> > email to byu-cs-330-fall-...@googlegroups.com.

>> >> > For more options, visit https://groups.google.com/groups/opt_out.
>> >>
>> >>
>> >>
>> >> --
>> >> 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
>> >
>> >
>> > --
>> > You received this message because you are subscribed to the Google
>> > Groups
>> > "byu-cs-330-fall-2013" group.
>> > To unsubscribe from this group and stop receiving emails from it, send
>> > an

>> > email to byu-cs-330-fall-...@googlegroups.com.

>> > For more options, visit https://groups.google.com/groups/opt_out.
>>
>>
>>
>> --
>> 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
>
>
> --
> You received this message because you are subscribed to the Google Groups
> "byu-cs-330-fall-2013" group.
> To unsubscribe from this group and stop receiving emails from it, send an

> email to byu-cs-330-fall-...@googlegroups.com.

> For more options, visit https://groups.google.com/groups/opt_out.



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

--
You received this message because you are subscribed to the Google Groups "byu-cs-330-fall-2013" group.

To unsubscribe from this group and stop receiving emails from it, send an email to byu-cs-330-fall-...@googlegroups.com.

[Scott Heidbrink]

And then that would vet removed in the unification function correct? Unless it is polymorphic then it would continue past then?

[Jay McCarthy]

Yup

On Thu, Nov 28, 2013 at 4:41 PM, Scott Heidbrink
<scott.h...@gmail.com> wrote:
> And then that would vet removed in the unification function correct? Unless it is polymorphic then it would continue past then?
>

[Scott Heidbrink]

So since we add that new type does that mean we should change the (constraint-list=?) to add that new type? Does that make sense or am i going crazy here?

On Thursday, November 28, 2013 6:32:35 PM UTC-7, Jay McCarthy wrote:

Yup

On Thu, Nov 28, 2013 at 4:41 PM, Scott Heidbrink
<scott.h...@gmail.com> wrote:
> And then that would vet removed in the unification function correct? Unless it is polymorphic then it would continue past then?
>
> --
> You received this message because you are subscribed to the Google Groups "byu-cs-330-fall-2013" group.

> To unsubscribe from this group and stop receiving emails from it, send an email to byu-cs-330-fall-2013+unsub...@googlegroups.com.

[Scott Heidbrink]

and by should i mean could

[Jay McCarthy]

You are crazy. You add a new type variable: (t-var (gensym 'newthing))

Jay

On Fri, Nov 29, 2013 at 12:27 AM, Scott Heidbrink
<scott.h...@gmail.com> wrote:
> So since we add that new type does that mean we should change the
> (constraint-list=?) to add that new type? Does that make sense or am i going
> crazy here?
>
>
> On Thursday, November 28, 2013 6:32:35 PM UTC-7, Jay McCarthy wrote:
>>
>> Yup
>>
>> On Thu, Nov 28, 2013 at 4:41 PM, Scott Heidbrink
>> <scott.h...@gmail.com> wrote:
>> > And then that would vet removed in the unification function correct?
>> > Unless it is polymorphic then it would continue past then?
>> >
>> > --
>> > You received this message because you are subscribed to the Google
>> > Groups "byu-cs-330-fall-2013" group.
>> > To unsubscribe from this group and stop receiving emails from it, send

>> > an email to byu-cs-330-fall-...@googlegroups.com.

>> > For more options, visit https://groups.google.com/groups/opt_out.
>>
>>
>>
>> --
>> 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
>

> --
> You received this message because you are subscribed to the Google Groups
> "byu-cs-330-fall-2013" group.
> To unsubscribe from this group and stop receiving emails from it, send an

> email to byu-cs-330-fall-...@googlegroups.com.

[Scott Heidbrink]

O hey that makes a lot more sense than what I was doing...oops....thanks

[Ben Draut]

So if I understand this correctly, tempty will always be constrained as a (t-list (t-var (gensym 'some-new-variable))) ?

On Fri, Nov 29, 2013 at 11:16 AM, Scott Heidbrink <scott.h...@gmail.com> wrote:

O hey that makes a lot more sense than what I was doing...oops....thanks

[Jay McCarthy]

Ya

[Jay McCarthy]

Yes

On Tue, Dec 3, 2013 at 9:50 AM, Ben Draut <dra...@gmail.com> wrote:
> In regular Racket, calling first or rest on empty is a contract violation,
> but it will compile. I'm thinking that in our type inferrer, (tfirst tempty)
> or (trest tempty) shouldn't error because tempty is a list, but at runtime
> it would fail, just like Racket. Is that correct?