Is this correct?

[Willard Hagen]

Does this look good?

(generate-constraints 'top (parse '(bif (iszero 0) 1 2)))

(list

 (eqc (t-var 'top) (t-var 'bif92100))

 (eqc (t-var 'bif92100) (t-var 'iszero92101))

 (eqc (t-var 'iszero92101) (t-num))

 (eqc (t-var 'bif92100) (t-num))

 (eqc (t-var 'bif92100) (t-num)))

--
-Willard

[Jay McCarthy]

No. The condition must be a boolean.

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

iszero : num -> bool

On Mon, Dec 2, 2013 at 5:53 PM, Willard Hagen <willar...@gmail.com> wrote:
> Ok. That means I need to make my iszero into a boolean.
>
> Right now I am making
> (list (eqc (t-var 'top) (t-var 'iszero100158))
> (eqc (t-var 'iszero100158) (t-num)))
>
> from
>
> (generate-constraints 'top (parse '(iszero 0)))
>
> I am unsure of what iszero should look like from a generate-constraint call.
> Do you have any hints?
> Thanks!

[Jay McCarthy]

No. That doesn't constrain the input.

On Mon, Dec 2, 2013 at 6:21 PM, Willard Hagen <willar...@gmail.com> wrote:
> So it should look like this:
>
> (list (eqc (t-var 'top) (t-var 'iszero119105))
> (eqc (t-var 'iszero119105) (t-bool)))

[Jay McCarthy]

It is implausible that that would come out of a single call to
generate-constraints.

It is clearly wrong because the program should type check and it has
Num = Bool which doesn't unify.

Why would you think that works? What process are you using to come up
with these choices?

This is everything you need to know:

"iszero : num -> bool"

That means that the expression must be a bool, because it is the
output of iszero, and that the argument to iszero must be a number,
then you'll get all the constraints from the argument expression too.

Jay


On Mon, Dec 2, 2013 at 7:25 PM, Willard Hagen <willar...@gmail.com> wrote:
> So is it this?

>
> (list
> (eqc (t-var 'top) (t-var 'iszero100158))
> (eqc (t-var 'iszero100158) (t-num))

> (eqc (t-num) (t-bool)))

[Jay McCarthy]

That's totally wrong. You have:

X = Y
Y = Num
Y = Bool

which means that Num = Bool

which means the constraints don't unify and the program is wrong, but
we know a priori it is right.

Jay

On Mon, Dec 2, 2013 at 7:55 PM, Willard Hagen <willar...@gmail.com> wrote:
> I don't think I understand this. I read that the output is last so, I think
> that

>
> (list
> (eqc (t-var 'top) (t-var 'iszero100158))
> (eqc (t-var 'iszero100158) (t-num))

> (eqc (t-var 'iszero100158) (t-bool)))
>
> Is correct because the final eqc of the iszero is a bool, meaning it is the
> output.

[Willard Hagen]

Ok.  So When I do a  (eqc (t-var 'top) (t-var 'iszero100158))

                         

This means I am doing X = Y.  What would be  X -> Y?

And what would be A: X -> Y ?  I can't seem to find out how to do anything but X = Y

--
-Willard

[Jay McCarthy]

There is only one kind of constraint, eqc. If you want to say A = X ->
Y then you can represent it as (eqc (t-var 'a) (t-fun (t-var 'x)
(t-var 'y)))

Jay

[Jay McCarthy]

No, because the RESULT of the program isn't a function. But iszero
takes a number and returns a bool. So the result of the whole program
is the bool.

On Mon, Dec 2, 2013 at 9:47 PM, Willard Hagen <willar...@gmail.com> wrote:
> So if I were to start with iszero, it would be:
> (list
> (eqc (t-var 'top) (t-var 'iszero20))
> (eqc (t-var 'iszero20) (t-fun (t-num) (t-bool))))

[Jay McCarthy]

What list? The substitution is logically a map and has no ordering.

You are not writing an interpreter, so the result of the program will
never be computed.

On Tue, Dec 3, 2013 at 4:08 PM, Willard Hagen <willar...@gmail.com> wrote:
> Should the result of the program be at the end of the list?