Union and intersection contracts are hard(tweag.io)
tweag.io
Union and intersection contracts are hard
https://www.tweag.io/blog/2022-04-28-union-intersection-contracts/
11 comments
These operations are not hard, what’s hard is doing them in a lazy context like they describe: they’re trying to evaluate data without, you know, evaluating it. Good luck.
This seems closely related to exhaustive checking of functions. There are some functions that you can test by trying every possible input. (For example, a function that takes an int32.) But most functions can't be tested that way.
Obviously, static analysis is possible, but the type system needs to be designed with type-checking functions in mind.
Obviously, static analysis is possible, but the type system needs to be designed with type-checking functions in mind.
Thanks, I had the same thought when I reached the word “lazy”.
The paper also describes function contracts, which I think simply ensure that the return types and argument types conform to a specification. This isn’t lazy, per se, but in a dynamic language you can’t check those things until you call the function. But isn’t that an obvious point?
The paper also describes function contracts, which I think simply ensure that the return types and argument types conform to a specification. This isn’t lazy, per se, but in a dynamic language you can’t check those things until you call the function. But isn’t that an obvious point?
What is dynamic typing but lazy static typing?
It seems like "union" is often nonsensical for function types. They say it's useful for representing overloaded functions, but then give this example:
let f | ( Positive → Positive ) ∪ ( Positive → NonPositive ) = fun x ⇒ x - 7 in (f 10) + ( f 5)
Here a function is supposed to take a positive number and then return a number that's both positive and negative. That is, the intersection of the return types is the empty set and there's no possible implementation.
So it seems like arbitrary unions of multiple function types isn't a good way to represent a function type. But it's unclear why you'd expect this to work since taking the union of two functions doesn't work either. Considered as a set of (input, output) pairs, the union of two functions is often a nonfunction, mapping the same input to multiple outputs.
Consider how this works for merging dictionaries. Each key can only be mapped to one value, so you can't just take the union without deciding which input takes priority when keys overlap.
Similarly, for function overloading, either the input types don't overlap or there is some way of deciding which takes priority.
let f | ( Positive → Positive ) ∪ ( Positive → NonPositive ) = fun x ⇒ x - 7 in (f 10) + ( f 5)
Here a function is supposed to take a positive number and then return a number that's both positive and negative. That is, the intersection of the return types is the empty set and there's no possible implementation.
So it seems like arbitrary unions of multiple function types isn't a good way to represent a function type. But it's unclear why you'd expect this to work since taking the union of two functions doesn't work either. Considered as a set of (input, output) pairs, the union of two functions is often a nonfunction, mapping the same input to multiple outputs.
Consider how this works for merging dictionaries. Each key can only be mapped to one value, so you can't just take the union without deciding which input takes priority when keys overlap.
Similarly, for function overloading, either the input types don't overlap or there is some way of deciding which takes priority.
This sounds like the lessons of Prolog. And Prolog needs hints once it gets real. Naive search generates too large a space.
You know what? A brute-force formula finding engine I made, which I call the Guesser 2.0 (it's the second version), might speed that up a lot, like twice the number of symbols in the functions it finds, in the same amount of time.
Can you elaborate on the Prolog problem so I can tell if it's a good fit? Guesser 2.0 specifically reduces the search space of naive search.
Can you elaborate on the Prolog problem so I can tell if it's a good fit? Guesser 2.0 specifically reduces the search space of naive search.
Prolog is a declarative logic system. As a result, implementing something like a list equality operator means that you can also run the code in "reverse" -- generate a list that is equal to this list. But as soon as the problem becomes complicated, the order you traverse the search space, and which branches of the search space you exclude early are critical to practical solutions. Prolog solves with cuts and other hints.
A quick google produces this example - https://en.m.wikibooks.org/wiki/Prolog/Cuts_and_Negation https://www.cs.uleth.ca/~gaur/post/prolog-cut-negation/
A quick google produces this example - https://en.m.wikibooks.org/wiki/Prolog/Cuts_and_Negation https://www.cs.uleth.ca/~gaur/post/prolog-cut-negation/
Came in here intrigued for an interesting left wing discussion
I was expecting blockchain smart contracts being composed somehow using logical operations. That would have been kind of cool, as someone forced to become a cryptocurrency hater. Silly of me, really, to think they had started paying attention to PLT principles. :)
wait, what? This does not seem right. Python can easily deserialize millions of json records per second (and that involves much more that simple validation described in the article). And this talks about Haskell, which is compiled and should be much faster.
Was the decision to be "lazy", which caused so much more complexity, caused by bad assumptions and lack of benchmarking?
> If foo is never used, the contract won’t fail the execution.
This sounds like suboptimal developer's experience, you usually want to validate everything upfront. Spending 10 minutes compiling and then failing because of typo in install location sucks.