Multiple argument function for constraints

[Derrick Brinton]

When you're generating a constraint, how do you represent a function
that takes in two arguments. For example, you might have:

1. (cons
2. x
3. y)

This would take in two arguments, of type [[2]] and [[3]] and return
type [[1]]. How do we write that? For a single argument, it's more
obvious:

1. (first
2, x)

[[(first x)]] = [[x]] -> [[1]]

Am I doing this wrong? If not, then how should I represent the cons?

[Jesse J]

Have you read chapter 30.4 of the PLAI book? That might be what you're looking for. I believe it should be:

[[(cons x y)]] = [[x]] X [[y]] -> [[1]]

[Bryan Morse]

That's correct. We use the Cartesian product notation you hopefully saw in CS 236. We treat the multiple inputs as a single tuple, which is an element of the set defined by the Cartesian product of the type of the first input and the type of the second input (and extend that for more inputs).

For this one, though, you already know the type signatures of cons and can just generate the constraints one by one for the inputs (much like the table on p. 277 of your textbook):

[[y]] = list ( [[x]] )
[[1]] = [[y]]

Notice that this works regardless of what [[x]] is as long as everything is consistent when unified with all of the other constraints (i.e., you use it consistently).