Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Type checking is suspectible to exponential blowup #168

Open
Shimuuar opened this issue Oct 12, 2020 · 3 comments
Open

Type checking is suspectible to exponential blowup #168

Shimuuar opened this issue Oct 12, 2020 · 3 comments

Comments

@Shimuuar
Copy link
Contributor

Let consider following program:

let x0 = 1
let x1 = (x0,x0)
let x2 = (x1,x1)
...
let x[N] = (x[N-1], x[N-1])
in x[N]

type of x[N] is nested tuple with 2^N leaves. Note it won't use exponential memory because of sharing. Still it's possible to make type checker effectively hang by comparing with type by equality with itself. Maybe it's even possible to break sharing and crash type checker by exhausting memory

It seems only way out is to place limit on depth of nesting in types and tuple size. Such limits are necessarily arbitrary so it's not obvious how they should be chosen.

@Shimuuar
Copy link
Contributor Author

On second thought limit by depth doesn't work very well since we can have both function which could have rather deep nesting with very low fanout. Take for example type A → A → ... → A → A which essentially represented as type list, while nested tuples could be very wide and genereate large types with modest nesting. So only viable way to limit size of data type using number of constructors as metric

@anton-k
Copy link
Contributor

anton-k commented Oct 13, 2020

Can we solve this problem with requirement of explicit type-signatures for let-expressions and maybe for arguments of lambda-expressions?

@Shimuuar
Copy link
Contributor Author

It doesn't look like good solution to me since it will increase transaction size and we'll have to check whether annotated type is equal to inferred. Lambda though have to be annotated. Effectively this outsources type size check to transaction size check.

On one hand it's possible it likely will solve problem of types blowup. It still could be possible to introduce growing types. While it seems unlikely I cant rule it out. So far I slightly in favor of limiting maximum size of type. Size could be cached in nodes of type ast during its construction and approach is relatively foolproof

P.S. On related note we may also have to beware quadratic performance as well. It's not quite catastrophic as exponential but still has potential to be used as DoS vector

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants