Timeline for Dependent C-style types with subtyping rule
Current License: CC BY-SA 4.0
18 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Mar 2, 2019 at 9:01 | vote | accept | Francesco Bertolaccini | ||
| Mar 1, 2019 at 0:21 | answer | added | xrq | timeline score: 1 | |
| Mar 1, 2019 at 0:01 | comment | added | xrq | @FrancescoBertolaccini Hm, I believe that you can still use the same setup. You still have Liquid Types, except that your language of constraints is highly constrained. This way you can replace the SMT solver with a built-in, less-capable solver. OTOH, if you don't have very complex constraints, maybe you're better off using symbolic execution or abstract interpretation, rather than extending the type system? | |
| Feb 28, 2019 at 17:18 | comment | added | Francesco Bertolaccini | @xuq01 Linear arithmetic is not to be allowed, I plan on only providing "bound" constraints of the type I've shown in the examples. I believe the limitedness of the language would make it restrictive, yes, but also useful in some specific applications. | |
| Feb 28, 2019 at 16:49 | comment | added | xrq | If you only allow the constraints of a very weak form, I suppose you can do it in polynomial time. But then you gain very little from the constraints on types. | |
| Feb 28, 2019 at 16:46 | comment | added | xrq | @FrancescoBertolaccini I believe that as long as you have linear arithmetic constraints in types, you can't do it in polynomial time anymore (of course, unless P=NP). Integer programming is NP-complete, so if you allow arithmetic constraints in types, they might not be solvable in polynomial time. | |
| Feb 28, 2019 at 9:00 | comment | added | Francesco Bertolaccini | @xuq01 the issue I've found with liquid types is that they are still basically dependent types and they require an SMT solver in most cases, I'm working on doing something that is decidable preferably in polynomial time | |
| Feb 28, 2019 at 8:38 | comment | added | xrq | The state of art in this realm is definitely Liquid Haskell. Play with it and have fun hacking! | |
| Feb 28, 2019 at 8:37 | comment | added | xrq | I think refinement types are exactly what you want. | |
| Feb 27, 2019 at 7:33 | comment | added | Francesco Bertolaccini | @jmite That's indeed probably as close as it's going to get, thank you! You should probably add it as an answer | |
| Feb 26, 2019 at 15:10 | comment | added | Joey Eremondi | Take a look at Dependent ML, it seems similar to what you're dealing with. | |
| Feb 26, 2019 at 12:41 | comment | added | Francesco Bertolaccini | @MartinBerger refinement types look interesting, I'll read up on them and I'll come back once I know something more about them | |
| Feb 26, 2019 at 11:28 | comment | added | Martin Berger | Could refinement types be what you are looking for? | |
| Feb 26, 2019 at 11:02 | comment | added | Francesco Bertolaccini | @MartinBerger I've added some edits in regards to your comment. Indeed, pointers are a bit out of scope for my idea | |
| Feb 26, 2019 at 11:01 | history | edited | Francesco Bertolaccini | CC BY-SA 4.0 |
Clarification in response to comment
|
| Feb 26, 2019 at 10:56 | comment | added | Martin Berger | What do you man by C-style types? C has pointer types, which are generally a bit difficult to reconcile with interesting type-safety properties. | |
| Feb 26, 2019 at 10:50 | review | First posts | |||
| Feb 28, 2019 at 7:55 | |||||
| Feb 26, 2019 at 10:49 | history | asked | Francesco Bertolaccini | CC BY-SA 4.0 |