Skip to content
This repository has been archived by the owner on Jun 1, 2022. It is now read-only.

Refinement types #16

Open
jonhue opened this issue Oct 16, 2020 · 0 comments
Open

Refinement types #16

jonhue opened this issue Oct 16, 2020 · 0 comments
Labels
proposal New proposal for the language spec
Milestone
0.2.0

Comments

@jonhue
Copy link
Member

jonhue commented Oct 16, 2020 •
edited
Loading 

[type_pattern | predicate, predicate, ...]

# example
[x: Number | x > 0]

GreaterThan = (T, x: T) [y: T | y > x]
[(a: Type, Type) | a > 0, a < 10]

A type pattern is any type that may include x ~ Type.

Use Z3 as SMT solver.

Resources

https://en.wikipedia.org/wiki/Hoare_logic
https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence#General_formulation
http://goto.ucsd.edu/~rjhala/liquid/liquid_types.pdf
http://strictlypositive.org/Easy.pdf
http://www.cs.nott.ac.uk/~psztxa/publ/ydtm.pdf

Caveats

We need to ensure that pattern matching on refined types is exhaustive.
@jonhue jonhue assigned jonhue and unassigned jonhue Oct 16, 2020
@jonhue jonhue transferred this issue from tony-lang/tree-sitter-tony Nov 12, 2020
@jonhue jonhue added discussion Has not been decided upon yet proposal New proposal for the language spec labels Nov 12, 2020
@jonhue jonhue added this to the 0.3.0 milestone Nov 12, 2020
@jonhue jonhue removed the discussion Has not been decided upon yet label Dec 15, 2020
@jonhue jonhue mentioned this issue Dec 15, 2020
Closed
@jonhue jonhue modified the milestones: 0.3.0, 0.2.0 Dec 15, 2020
@jonhue jonhue mentioned this issue Dec 15, 2020
Closed
@jonhue jonhue added this to Core Nov 19, 2021
@jonhue jonhue moved this to In Progress in Core Nov 19, 2021
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Assignees
No one assigned
Labels
proposal New proposal for the language spec
Projects
Core
Status: In Progress
Milestone
0.2.0
Development

No branches or pull requests
1 participant
@jonhue