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

Simple refinement types #638

Merged
merged 83 commits into from
Oct 10, 2019
Merged

Simple refinement types #638

merged 83 commits into from
Oct 10, 2019

Conversation

bvssvni
Copy link
Member

@bvssvni bvssvni commented Sep 15, 2019

Dyon is a rusty dynamically typed scripting language.

What are simple refinement types?

A simple refinement type system is an "extra layer" of types in addition to the normal type signature of functions. This is used to catch more errors before runtime.

The extra layer contains special knowledge about the function or alternative semantics from how the function is used.

Dyon supports ad-hoc types which lets you write e.g. Unknown bool instead of just bool. Simple refinement types in Dyon works seamlessly ad-hoc types.

For example, one can use this to type check many-valued boolean logic:

use std as std

fn flip() -> Unknown bool {return if random() < 0.5 {false} else {true}}
fn tr() -> True bool {return true}
fn fa() -> False bool {return false}

// Override `!` operator.
fn not(a: bool) -> bool {return std::not(a)}
    // Use simple refinement types to add extra type information.
    (True bool) -> False bool
    (False bool) -> True bool
    (Unknown bool) -> Unknown bool

fn check_tr(_: True bool) {}

fn main() {
    a := flip()
    check_tr(!a)
}

The ad-hoc type Unknown bool is constructed by a coin-flip. If you invert a coin-flip, you don't know whether it is true or false, so it is still Unknown bool.

Dyon detects an error in the code above:

Type mismatch (#100):
Expected `True bool`, found `Unknown bool`
17,14:     check_tr(!a)
17,14:              ^

In this example, I used simple refinement types to reason about nondeterministic behavior of many-valued boolean logic. Instead of writing code explicitly as many-valued boolean logic, one can use ad-hoc types to lift the many-value logic to type level.

Design

For design, see #636

This PR adds support for simple refinement types in Dyon. This allows e.g. binary operators to be type checked as external functions.

Improvements in performance

There is a 4.4% improvement in performance on the n-body benchmark for n=100_000. This is a longer run that is tested manually and measures performance on typical game-logic workloads.

For design, see PistonDevelopers#636

- Added “typechk/refinement.dyon”
- Added “typechk/refinement_2.dyon”
- Added “typechk/refinement_3.dyon”
- Added “typechk/refinement_4.dyon”
- Removed `Type::is_concrete`
- Added “typechk/refinement_5.dyon”
- Fixed bug `a.goes_with(b)` => `b.goes_with(a)`
- Added “typechk/refinement_6.dyon”
- Added “typechk/refinement_7.dyon”
- Swap order of `Type::ambiguous`
- Added “typechk/refinement_8.dyon”
- Added “typechk/refinement_9.dyon”
- Added “typechk/refinement_10.dyon”
- Added “typechk/refinement_11.dyon”
- Added “typechk/refinement_12.dyon”
- Added “typechk/refinement_13.dyon”
- Added “typechk/refinement_14.dyon”
- Added “typechk/refinement_15.dyon”
- Added “typechk/refinement_16.dyon”
- Added “typechk/refinement_17.dyon”
- Added “typechk/refinement_18.dyon”
- Added “typechk/refinement_19.dyon”
- Added “typechk/refinement_20.dyon”
- Added “typechk/refinement_21.dyon”
- Added “typechk/refinement_22.dyon”
- Added “typechk/refinement_23.dyon”
- Added “syntax/secret_fail.dyon”
… something

- Added “typechk/void_refinement.dyon”
- Added “typechk/refinement_24.dyon”
- Added “typechk/refinement_25.dyon”
- Added ambiguity check for wrapper types
- Fixed doc comment on `Type::ambiguous`
- Added “typechk/refinement_26.dyon”
- Added “typechk/refinement_27.dyon”
- Added “typechk/refine_type_fail_2.dyon”
- Added “typechk/closure_ad_hoc.dyon”
- Added `UnOpEpression::into_expression`
@bvssvni
Copy link
Member Author

bvssvni commented Sep 24, 2019

I'm happy with this PR now, except that it runs 14 ms slower on the n_body benchmark.

I'm happy with this PR now.

I also tested the n_body benchmark on n = 100_000 (2 best of 3 runs):

Before:
real 0m3.177s
user 0m3.143s
sys 0m0.012s

real 0m3.152s
user 0m3.135s
sys 0m0.009s

After:
real 0m4.466s
user 0m4.444s
sys 0m0.011s

real 0m4.550s
user 0m4.528s
sys 0m0.011s

That's 42% slower. The overhead is due to slower runtime, probably because LLVM is better to optimize with binary and unary operators known in advance.

I tried separating external function types for void and returns, but it did not help.

One idea is to use custom external functions for unary and binary operators.

@bvssvni
Copy link
Member Author

bvssvni commented Oct 2, 2019

The performance drop was due to a bug in div.

After:
real 0m3.019s
user 0m3.009s
sys 0m0.007s

real 0m3.025s
user 0m3.016s
sys 0m0.007s

It is 4.4% faster now.

@bvssvni bvssvni mentioned this pull request Oct 10, 2019
@bvssvni
Copy link
Member Author

bvssvni commented Oct 10, 2019

Merging.

@bvssvni bvssvni merged commit 78d2acc into PistonDevelopers:master Oct 10, 2019
@bvssvni bvssvni deleted the ty branch October 10, 2019 16:14
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

Successfully merging this pull request may close these issues.

1 participant