11 ms·

A Gentle Introduction to Liquid Types

138 points by marvinborner 3y ago

peepeepoopoo33 3y ago
Programming language design took a wrong turn with these extremely complicated type systems. They end up hurting developer productivity, and you spend more time fiddling with types than solving the problem at hand. We should be focusing on more effective forms of abstraction instead of types.
- deleted 3y ago
  [deleted]
- agumonkey 3y ago
  > more effective forms of abstraction instead of types do you have any in mind ? I often think about a blend of functional and OO as 'protocol graphs' but it's a faint idea for now
  - peepeepoopoo33 3y ago
    Array programming is an extremely powerful paradigm that is criminally underused outside of data science applications. It also feels like the full power of array programming hasn't been explored yet.
    - mostlylurks 3y ago
      Array programming doesn't really have much effect on how relevant a type system is for a particular language. At most it will let you make operations generic over the rank of the inputs (scalar, array, array of arrays, etc), which is nice, but the scalar values at the bottom of that hierarchy are subject to all the same factors that motivate the type systems present in any other modern language.
      - peepeepoopoo33 3y ago
        My point is that academic PL research has diverged significantly from the kinds of problems people are really facing. That's why we've seen array programming emerge organically to address a direct industry need, and it didn't come from the PL crowd at all.
        deleted 3y ago
        [deleted]
        joaogui1 3y ago
        APL started at Harvard (though it developed more in IBM) and even nowadays there's the ARRAY workshop co-located with one of the main PL conferences. The thing is that while array programming is amazing for some specific problems it's not going to help you make sure that you don't have memory errors, race conditions, or wrong states in your program
        peepeepoopoo33 3y ago
        The implementations of array programming in use today are quite different from APL, and they all came from industry. > it's not going to help you make sure that you don't have memory errors, race conditions Not only does array programming abstract away those kinds of errors, it also solves the problems that I care about: code that is faster, more expressive, and easier to read and write. Unwieldy type systems do not help me solve those problems.
        maxbond 3y ago
        I can see how array programming helps with certain memory errors, but I don't think it helps with race conditions. Whereas eg Rust ownership, borrowing, and lifetimes eliminate one class of race conditions (data races) in safe code. Type systems also enable optimizations that do make code faster. Eg monomorphization. Consider that JITs makes untyped code faster by inferring types at runtime. See also this comment https://news.ycombinator.com/item?id=37376010 https://news.ycombinator.com/item?id=37376010 I honestly can't make heads or tails of the idea that type systems don't help make code more expressive? They allow you to express your precise intent in a way that's legible to both humans and the compiler.
  - maxbond 3y ago
    This protocol graph idea sounds intriguing. I'd love to hear more about it if you're interested in sharing.
- maxbond 3y ago
  What languages are you talking about? I find that the weaker the type system the more I feel fiddling with it is a waste, eg Python, but I don't feel that way when I'm working with a strong type system that can not only help eliminate bugs but aid the compiler in analysis and actually deliver a better artefact, eg Rust. LSPs are a sort of middle ground where I derive a lot of the value from, and even weak type systems really help the analysis of the LSP. They make me immensely more productive. I've been writing a lot of TypeScript lately, and I may not have taken the plunge to the frontend if LSPs hadn't made it dramatically easier. So in that case the impact on my productivity is +100%.
  - kristopolous 3y ago
    I'm not the parent but at least for me, my #1 complaint is "whiny computer". Especially when dealing with someone else's code, it can be a ceremonial roadblock for moving data around that could easily be processed without issue but artificial constraints in order to service an orthodoxy have been erected to make things needlessly more brittle. In the name of reducing bugs, it in practice can often impose workarounds that increase the chance the confusion and more bugs. This isn't always the case but most of the time things are built in incompetent hands (including my own). Accommodating for this reality is probably the better move. Imposition of absolutist rules doesn't improve the behavior of incompetency, it just makes it more subversive and the defects it creates more insidious
    - maxbond 3y ago
      Hmm interesting. Are these projects that were originally untyped but then gradually typed later? I ask because I've not really encountered that, the most I've had to do is add asserts or ifs to help explain to the typechecker something that I could see as a human. A few times in a gradually typed language I've needed to add an ignore to a line. But it's been rare in my experience. I try not to think of it as whining, I try to think of it as the type checker helpfully pointing out, "hey, you haven't done your due diligence here." I ran into this advice when learning Rust and it made it much more pleasant. In the same way that you might chase a series of failing tests to finish a task, you can chase a series of type warnings. I have them integrated into my editor, so usually the "series" is length 1 because I'm knocking them out as they arise. The projects I've worked with that were previously untyped (Python SaaS backends), I never actually ran the type checker on the entire source code. But if I had a megabyte of type errors that weren't really going to provide value to the business, yeah that would feel like a waste of time. Unless we were having serious quality issues and it was between annotating the entire codebase and rewriting it from scratch, I'd leave well enough alone - it's a tool, not a religion. But the new code I'm checking in, that's getting annotated for sure. I don't really see types as arbitrary absolutist rules. They're the semantics of the language, they're the rules you're following whether you have a typechecker or not. And if you violate them you're gunnuh get bugs and crashes regardless. I too am a flawed human who frequently makes mistakes, and I like having them caught immediately, before I've even checked my code in.
- packetlost 3y ago
  [flagged]
- systems 3y ago
  complexity doesn't go away, you distribute it you either create a complex program, with simple language constructs, or a simple program with complex language constructs if you use only the simplest types, your program will be very complex, if you put all the complexity in types, your type system will be very complex you need to balance things i think OOP is the extreme where all the complexity is in the Object system (or types system) functional programming with complex types, i think give a nicer balance, where some logic goes into the program flow and some goes into types anyway balance is everything, keep things balanced , dont lean too much into any direction
  - dietr1ch 3y ago
    Well, intrinsic complexity can be split, but artificial complexity might be added on top of it. Languages and libraries that are well designed and compose better end up being great at taming complexity. Functional languages are made to compose better, but their popularity is a hint that they are not that simple to use effectively.
- qudat 3y ago
  Similar arguments here: https://bower.sh/typescript-terrible-for-library-developers https://bower.sh/typescript-terrible-for-library-developers As a library developer I spend substantially more time on making the types right than the actual implementation. It can be brutal at times.
  - IshKebab 3y ago
    Think of how much time you'd have to spend writing trivial tests instead if you didn't have an automated system to detect basic mistakes like typos and type confusion! I guess you can complain that Typescript forces you to spend time making sure your code meets a minimal bar of correctness...
    - meheleventyone 3y ago
      Library developers in particular should see type complexity as a warning that something isn’t great in the design. This seems largely an issue for libraries migrating to TS which isn’t a surprise.
- PartiallyTyped 3y ago
  I disagree. These "complicated" type-systems enable fearless refactoring and give you guarantees without cluttering your code with validation checks because, well, there is the guarantee that faulty states are not representable.
one-punch 3y ago
Liquid Types enabled a 6x speed up in high-performance parsing of UDP packets, according to "Scrap your Bounds Checks with Liquid Haskell" of Gabriella Gonzalez [1]. With Liquid Haskell, the bound checks are moved from runtime to compile time, semi-automatically handled by SMT-solvers. Static types help programmers to write correct programs faster, and the programs also run faster. As an aside, speeding up programs with static analysis (constrained dynamism) are also present in Mojo (a variant of Python) or Swift [2]. [1]: https://github.com/Gabriella439/slides/blob/main/liquidhaskell/slides.md https://github.com/Gabriella439/slides/blob/main/liquidhaske... "Scrap your Bounds Checks with Liquid Haskell" [2]: https://github.com/modularml/mojo/discussions/466 https://github.com/modularml/mojo/discussions/466 "Mojo and Dynamism"
- CyberDildonics 3y ago
  This seems to be a complication to haskell to fix a performance problem that is only in haskell.
  - andyferris 3y ago
    I don't think that's fair. Automated bounds checking exists in many languages (and most modern high-level languages). In Rust you might be incentivised to use unsafe blocks for array access in performance sensitive code. Julia has its `@inbounds` annotation. Some languages might not have an escape hatch at all. Automatically removing bounds checking where safe seems like a good goal, but in all but the most trivial cases its quite complex for the compiler to decide what's safe.
    - capitalsigma 3y ago
      It seems a little disingenuous to call something written in an obscure Haskell dialect a "high performance UDP packet parser"
      - maxbond 3y ago
        Why? Looks like they're doing realtime network monitoring for security purposes. Sounds like a high performance application to me. Haskell has a reputation for being slow, but the proof is in the pudding - and what's being asserted is that a stronger type system enables better optimization.
hansvm 3y ago
This sort of idea is why I sketched out pdv [0] in Zig. Even extremely simple type systems can handle arbitrary invariants when you are allowed to compute with those invariants at compile time. [0] https://github.com/hmusgrave/pdv https://github.com/hmusgrave/pdv
- danaugrs 3y ago
  Very cool idea - starred!
  - hansvm 3y ago
    Happy to help :)
dionian 3y ago
reminds me a little of eiffel's design by contract. it looks really promising
- nextos 3y ago
  Your intuition is right. Liquid (refinement) types, design by contract and Hoare logic have, essentially, the same expressiveness. Personally I find refinement types more promising than dependent types, but time will tell.
- tgv 3y ago
  It made me wonder too, what the (practical) advantage over contracts is. If anything, Liquid Types seem less powerful. E.g., you can't use it to express a relation between two function parameters. It seems to be a macro for contracts (the type name implicitly copies its restriction as a contract clause), so in that sense it could be welcome as a practical way of improving correctness.
A_D_E_P_T 3y ago
I honestly thought that this was going to be about actual liquid types -- from the regular ones that (macroscopically) differ largely in terms of viscosity, to non-Newtonian liquids which have non-linear viscosity characteristics, to long-chain (PEG-type) polymers that have slightly unusual flow characteristics, to superfluids that have extremely weird characteristics and zero viscosity. ...I'd read that article. Now I'm starting to think that I should write it.
- rytill 3y ago
  I’d read it! That sounds really interesting.
- Modified3019 3y ago
  Had the exact same assumption, definitely still interested in something like that.
__vec__ 3y ago
DML link in the article is broken - Might I instead point you to a relevant ATS-lang (successor2 of DML) documentation about `Dependent Types in ATS2` https://ats-lang.sourceforge.net/DOCUMENT/INTPROGINATS/HTML/c2100.html https://ats-lang.sourceforge.net/DOCUMENT/INTPROGINATS/HTML/... This link discusses, along with other usefulness, the use of dependent types for the likes of array bounds checking, creating "sorts" of numbers satisfying various predicates, and more interestingly the utility of combining Dependent Types with PURE Linear Types (as opposed to Affine Types a la Rust lol) ... AFAIK, DML was originally intended as a gateway to constructing typed assembly (DARPA) Having been a researcher in this field for, this quote from the original paper on 'Liquid Types' originally seemed suspect.... "a system that combines Hindley-Milner type inference with Predicate Abstraction to automatically infer dependent types precise enough to prove a variety of safety properties" .... type inference with dependent types is undecidable!? Then again, this is one of the primary focuses of ATS3, I digress... This area of research is rich in pipe-dreams and cerebral investigation. From my biased opinion, ATS3 (the current version of the successor3 of DML, being actively devloped by the PI Professor Hongwei Xi, is the only language in this space to be aimed at practical programming in industry... of course there is always haskell....) What I mean is that, TEMPLATES++ Linear Types + Dependent Types + Hindley Milner Type inference .... At the end of the day, who doesn't love hyper efficient meta-programming magic?
- doublec 3y ago
  ATS is great, I’ve used ATS1 and ATS2 quite a bit and it worked well. Unfortunately it suffers a bit from the “rewrite every few years” as research directions change.
quickthrower2 3y ago
I like this sort of idea for typifying dynamic languages (like JS) What if instead of TS, you had plain JS as-is (no compiler needed!) then just add comment like: /* x is an integer, x > 0 ... */ function add(x, y) { ... Sorry the example ain't great but the point is that you can be precise with refinement types. I think refinement types (less all the mathy explanations) are more intuitive. They would be like assertions or C# code contracts. The content of those types would look "business-ey" rather than "category theory-ish".
- __vec__ 3y ago
  The difference is an informative error message at compile time when such fails to satisfy the 'refinement'
richard_fey 3y ago
How do you define operations on these liquid types? You can't even define subtraction or addition on this "non zero integer type". These types are not closed so how is it useful?
- maxbond 3y ago
  Addition isn't a problem, any nonzero integer plus a nonzero integer is a nonzero integer. For subtraction it becomes fallible. You get back an option, 5 - 4 = Some(1), 4 - 5 = None. (These are probably methods rather than infix operators, your language may vary.) See for example the methods documented here: https://doc.rust-lang.org/stable/std/num/struct.NonZeroUsize.html https://doc.rust-lang.org/stable/std/num/struct.NonZeroUsize... As for it's utility, it enables certain optimizations and it can be a useful constraint. Eg for ensuring that you don't divide or multiply by zero.
  - pharmakom 3y ago
    It would be in interred ring to have a memory bounds for the program too!
  - zokier 3y ago
    It is worth pointing out that the same problems apply to "normal" integer types like int32/uint32; you can trivially over/underflow the bounds with basic arithmetic. In that sense it doesn't really matter what the bounds are exactly.
  - School-Cotton 3y ago
    > any nonzero integer plus a nonzero integer is a nonzero integer That’s not true. 5 + (-5) is 0.
    - maxbond 3y ago
      You're right, I was thinking of a nonzero unsigned integer. D'oh! Thanks for the correction!
- saithound 3y ago
skybrian 3y ago
An important thing to remember about fancy type systems is that they can only make guarantees in a closed world. If your data comes from the network or a file, you will likely need a reader or parser that does runtime checks somewhere, but a good type system can provide assurance that you did each check exactly once. On a complicated single-process system (a monolith), that can be a big improvement. For distributed systems (microservices), there will still be plenty of runtime checks. That's what allows each service to have its own lifecycle. I'm wondering what Elixir will do, given that Erlang servers divide up work into lots of independent, distributed components?
- shepherdjerred 3y ago
  This is a fantastic point, and a huge issue that I had with TypeScript. Libraries for TypeScript like Zod[0] allow you to define types and validate against them at runtime. For example: https://stackblitz.com/edit/typescript-pwzng4?file=index.ts https://stackblitz.com/edit/typescript-pwzng4?file=index.ts At work, we use this to validate API responses, local storage contents, or URL/router data. It solves the problem you described -- dirty data coming from outside of the type system. This isn't a plug for Zod or TypeScript -- there are other similar libraries for TypeScript, and I would imagine other statically typed languages have something to fill this role. [0]: https://zod.dev/ https://zod.dev/
  - svrtknst 3y ago
    TypeScript became so much more pleasant to use after we started using parsers regularly. We use Runtypes in some projects and a hand rolled lib I wrote in others, and being able to parse unknown data into a known shape is a life saver. Glad to not have to write seemingly thousands of lines of interfaces and type guards any more.
  - diarrhea 3y ago
    Two random thoughts: - why is there `safeParse`? Why is parsing not safe by default? Have an `unsafeParse` as an escape hatch, not the other way around. - the imperative check for `success` seems unfortunate. Then again, I am familiar with pydantic from Python, which seems awfully similar to Zod, and there you'd get an Exception on failure which you'd have to catch. Some would call that uglier (I don't). Point being, I don't know of a better alternative, but sure hope native liquid/dependent types wouldn't suffer from this anymore
everybodyknows 3y ago
Title needs to append (2015).
eithed 3y ago
If Int (without 0) should be used, why not use IntWithoutZero type?
LeanderK 3y ago
I wonder how pragmatic those can become. Usually I don't really care about "exact" exactness, a common theme in haskell. A sort of "under common assumptions" (no underflow/overflow/OOM etc.) proof of laws and properties. This eliminates a whole class of bugs and strengthens your ability to reason, but doesn't make everything super, super complicated by thinking about all those edge cases. One usually doesn't program airplane control software. Some bugs are okay and speed of development and correctness is a trade-off.
mabbo 3y ago
I wonder what is possible in more common languages like Java or Python. Certainly, the language itself won't have liquid types in the compiler any time soon. But taking Ruby's Sorbet as inspiration, I wonder if you could annotate Java classes with semantic rules and do some simple verifications as a post-compilation step? There's too much bad code out there that can't just be replaced. Tools to help make it better would be a huge boon.
- c-cube 3y ago
  In 2008 at univ I had a few classes using http://krakatoa.lri.fr/ http://krakatoa.lri.fr/. Tools definitely exist, although you could probably argue that the production ready version of that that people use in practice is really Ada/SPARK (built on similar technologies if not the same)
- sn9 3y ago
  Java has JML [0] and Python has all sorts of DBC libraries that can accomplish something similar [1]. [0] https://www.thestrangeloop.com/2018/contracts-for-getting-more-programs-less-wrong.html https://www.thestrangeloop.com/2018/contracts-for-getting-mo... [1] https://www.hillelwayne.com/talks/beyond-unit-tests/ https://www.hillelwayne.com/talks/beyond-unit-tests/

138 points by marvinborner 3y ago

Programming language design took a wrong turn with these extremely complicated type systems. They end up hurting developer productivity, and you spend more time fiddling with types than solving the problem at hand. We should be focusing on more effective forms of abstraction instead of types.

deleted 3y ago
[deleted]
agumonkey 3y ago
> more effective forms of abstraction instead of types do you have any in mind ? I often think about a blend of functional and OO as 'protocol graphs' but it's a faint idea for now
- peepeepoopoo33 3y ago
  Array programming is an extremely powerful paradigm that is criminally underused outside of data science applications. It also feels like the full power of array programming hasn't been explored yet.
  - mostlylurks 3y ago
    Array programming doesn't really have much effect on how relevant a type system is for a particular language. At most it will let you make operations generic over the rank of the inputs (scalar, array, array of arrays, etc), which is nice, but the scalar values at the bottom of that hierarchy are subject to all the same factors that motivate the type systems present in any other modern language.
    - peepeepoopoo33 3y ago
      My point is that academic PL research has diverged significantly from the kinds of problems people are really facing. That's why we've seen array programming emerge organically to address a direct industry need, and it didn't come from the PL crowd at all.
      - deleted 3y ago
        [deleted]
      - joaogui1 3y ago
        APL started at Harvard (though it developed more in IBM) and even nowadays there's the ARRAY workshop co-located with one of the main PL conferences. The thing is that while array programming is amazing for some specific problems it's not going to help you make sure that you don't have memory errors, race conditions, or wrong states in your program
        peepeepoopoo33 3y ago
        The implementations of array programming in use today are quite different from APL, and they all came from industry. > it's not going to help you make sure that you don't have memory errors, race conditions Not only does array programming abstract away those kinds of errors, it also solves the problems that I care about: code that is faster, more expressive, and easier to read and write. Unwieldy type systems do not help me solve those problems.
        maxbond 3y ago
        I can see how array programming helps with certain memory errors, but I don't think it helps with race conditions. Whereas eg Rust ownership, borrowing, and lifetimes eliminate one class of race conditions (data races) in safe code. Type systems also enable optimizations that do make code faster. Eg monomorphization. Consider that JITs makes untyped code faster by inferring types at runtime. See also this comment https://news.ycombinator.com/item?id=37376010 https://news.ycombinator.com/item?id=37376010 I honestly can't make heads or tails of the idea that type systems don't help make code more expressive? They allow you to express your precise intent in a way that's legible to both humans and the compiler.
- maxbond 3y ago
  This protocol graph idea sounds intriguing. I'd love to hear more about it if you're interested in sharing.
maxbond 3y ago
What languages are you talking about? I find that the weaker the type system the more I feel fiddling with it is a waste, eg Python, but I don't feel that way when I'm working with a strong type system that can not only help eliminate bugs but aid the compiler in analysis and actually deliver a better artefact, eg Rust. LSPs are a sort of middle ground where I derive a lot of the value from, and even weak type systems really help the analysis of the LSP. They make me immensely more productive. I've been writing a lot of TypeScript lately, and I may not have taken the plunge to the frontend if LSPs hadn't made it dramatically easier. So in that case the impact on my productivity is +100%.
- kristopolous 3y ago
  I'm not the parent but at least for me, my #1 complaint is "whiny computer". Especially when dealing with someone else's code, it can be a ceremonial roadblock for moving data around that could easily be processed without issue but artificial constraints in order to service an orthodoxy have been erected to make things needlessly more brittle. In the name of reducing bugs, it in practice can often impose workarounds that increase the chance the confusion and more bugs. This isn't always the case but most of the time things are built in incompetent hands (including my own). Accommodating for this reality is probably the better move. Imposition of absolutist rules doesn't improve the behavior of incompetency, it just makes it more subversive and the defects it creates more insidious
  - maxbond 3y ago
    Hmm interesting. Are these projects that were originally untyped but then gradually typed later? I ask because I've not really encountered that, the most I've had to do is add asserts or ifs to help explain to the typechecker something that I could see as a human. A few times in a gradually typed language I've needed to add an ignore to a line. But it's been rare in my experience. I try not to think of it as whining, I try to think of it as the type checker helpfully pointing out, "hey, you haven't done your due diligence here." I ran into this advice when learning Rust and it made it much more pleasant. In the same way that you might chase a series of failing tests to finish a task, you can chase a series of type warnings. I have them integrated into my editor, so usually the "series" is length 1 because I'm knocking them out as they arise. The projects I've worked with that were previously untyped (Python SaaS backends), I never actually ran the type checker on the entire source code. But if I had a megabyte of type errors that weren't really going to provide value to the business, yeah that would feel like a waste of time. Unless we were having serious quality issues and it was between annotating the entire codebase and rewriting it from scratch, I'd leave well enough alone - it's a tool, not a religion. But the new code I'm checking in, that's getting annotated for sure. I don't really see types as arbitrary absolutist rules. They're the semantics of the language, they're the rules you're following whether you have a typechecker or not. And if you violate them you're gunnuh get bugs and crashes regardless. I too am a flawed human who frequently makes mistakes, and I like having them caught immediately, before I've even checked my code in.
packetlost 3y ago
[flagged]
systems 3y ago
complexity doesn't go away, you distribute it you either create a complex program, with simple language constructs, or a simple program with complex language constructs if you use only the simplest types, your program will be very complex, if you put all the complexity in types, your type system will be very complex you need to balance things i think OOP is the extreme where all the complexity is in the Object system (or types system) functional programming with complex types, i think give a nicer balance, where some logic goes into the program flow and some goes into types anyway balance is everything, keep things balanced , dont lean too much into any direction
- dietr1ch 3y ago
  Well, intrinsic complexity can be split, but artificial complexity might be added on top of it. Languages and libraries that are well designed and compose better end up being great at taming complexity. Functional languages are made to compose better, but their popularity is a hint that they are not that simple to use effectively.
qudat 3y ago
Similar arguments here: https://bower.sh/typescript-terrible-for-library-developers https://bower.sh/typescript-terrible-for-library-developers As a library developer I spend substantially more time on making the types right than the actual implementation. It can be brutal at times.
- IshKebab 3y ago
  Think of how much time you'd have to spend writing trivial tests instead if you didn't have an automated system to detect basic mistakes like typos and type confusion! I guess you can complain that Typescript forces you to spend time making sure your code meets a minimal bar of correctness...
  - meheleventyone 3y ago
    Library developers in particular should see type complexity as a warning that something isn’t great in the design. This seems largely an issue for libraries migrating to TS which isn’t a surprise.
PartiallyTyped 3y ago
I disagree. These "complicated" type-systems enable fearless refactoring and give you guarantees without cluttering your code with validation checks because, well, there is the guarantee that faulty states are not representable.

one-punch 3y ago

Liquid Types enabled a 6x speed up in high-performance parsing of UDP packets, according to "Scrap your Bounds Checks with Liquid Haskell" of Gabriella Gonzalez [1]. With Liquid Haskell, the bound checks are moved from runtime to compile time, semi-automatically handled by SMT-solvers. Static types help programmers to write correct programs faster, and the programs also run faster. As an aside, speeding up programs with static analysis (constrained dynamism) are also present in Mojo (a variant of Python) or Swift [2]. [1]: https://github.com/Gabriella439/slides/blob/main/liquidhaskell/slides.md https://github.com/Gabriella439/slides/blob/main/liquidhaske... "Scrap your Bounds Checks with Liquid Haskell" [2]: https://github.com/modularml/mojo/discussions/466 https://github.com/modularml/mojo/discussions/466 "Mojo and Dynamism"

CyberDildonics 3y ago
This seems to be a complication to haskell to fix a performance problem that is only in haskell.
- andyferris 3y ago
  I don't think that's fair. Automated bounds checking exists in many languages (and most modern high-level languages). In Rust you might be incentivised to use unsafe blocks for array access in performance sensitive code. Julia has its `@inbounds` annotation. Some languages might not have an escape hatch at all. Automatically removing bounds checking where safe seems like a good goal, but in all but the most trivial cases its quite complex for the compiler to decide what's safe.
  - capitalsigma 3y ago
    It seems a little disingenuous to call something written in an obscure Haskell dialect a "high performance UDP packet parser"
    - maxbond 3y ago
      Why? Looks like they're doing realtime network monitoring for security purposes. Sounds like a high performance application to me. Haskell has a reputation for being slow, but the proof is in the pudding - and what's being asserted is that a stronger type system enables better optimization.

hansvm 3y ago

This sort of idea is why I sketched out pdv [0] in Zig. Even extremely simple type systems can handle arbitrary invariants when you are allowed to compute with those invariants at compile time. [0] https://github.com/hmusgrave/pdv https://github.com/hmusgrave/pdv

danaugrs 3y ago
Very cool idea - starred!
- hansvm 3y ago
  Happy to help :)

dionian 3y ago

reminds me a little of eiffel's design by contract. it looks really promising

nextos 3y ago
Your intuition is right. Liquid (refinement) types, design by contract and Hoare logic have, essentially, the same expressiveness. Personally I find refinement types more promising than dependent types, but time will tell.
tgv 3y ago
It made me wonder too, what the (practical) advantage over contracts is. If anything, Liquid Types seem less powerful. E.g., you can't use it to express a relation between two function parameters. It seems to be a macro for contracts (the type name implicitly copies its restriction as a contract clause), so in that sense it could be welcome as a practical way of improving correctness.

A_D_E_P_T 3y ago

I honestly thought that this was going to be about actual liquid types -- from the regular ones that (macroscopically) differ largely in terms of viscosity, to non-Newtonian liquids which have non-linear viscosity characteristics, to long-chain (PEG-type) polymers that have slightly unusual flow characteristics, to superfluids that have extremely weird characteristics and zero viscosity. ...I'd read that article. Now I'm starting to think that I should write it.

rytill 3y ago
I’d read it! That sounds really interesting.
Modified3019 3y ago
Had the exact same assumption, definitely still interested in something like that.

__vec__ 3y ago

DML link in the article is broken - Might I instead point you to a relevant ATS-lang (successor2 of DML) documentation about `Dependent Types in ATS2` https://ats-lang.sourceforge.net/DOCUMENT/INTPROGINATS/HTML/c2100.html https://ats-lang.sourceforge.net/DOCUMENT/INTPROGINATS/HTML/... This link discusses, along with other usefulness, the use of dependent types for the likes of array bounds checking, creating "sorts" of numbers satisfying various predicates, and more interestingly the utility of combining Dependent Types with PURE Linear Types (as opposed to Affine Types a la Rust lol) ... AFAIK, DML was originally intended as a gateway to constructing typed assembly (DARPA) Having been a researcher in this field for, this quote from the original paper on 'Liquid Types' originally seemed suspect.... "a system that combines Hindley-Milner type inference with Predicate Abstraction to automatically infer dependent types precise enough to prove a variety of safety properties" .... type inference with dependent types is undecidable!? Then again, this is one of the primary focuses of ATS3, I digress... This area of research is rich in pipe-dreams and cerebral investigation. From my biased opinion, ATS3 (the current version of the successor3 of DML, being actively devloped by the PI Professor Hongwei Xi, is the only language in this space to be aimed at practical programming in industry... of course there is always haskell....) What I mean is that, TEMPLATES++ Linear Types + Dependent Types + Hindley Milner Type inference .... At the end of the day, who doesn't love hyper efficient meta-programming magic?

doublec 3y ago
ATS is great, I’ve used ATS1 and ATS2 quite a bit and it worked well. Unfortunately it suffers a bit from the “rewrite every few years” as research directions change.

quickthrower2 3y ago

I like this sort of idea for typifying dynamic languages (like JS) What if instead of TS, you had plain JS as-is (no compiler needed!) then just add comment like: /* x is an integer, x > 0 ... */ function add(x, y) { ... Sorry the example ain't great but the point is that you can be precise with refinement types. I think refinement types (less all the mathy explanations) are more intuitive. They would be like assertions or C# code contracts. The content of those types would look "business-ey" rather than "category theory-ish".

__vec__ 3y ago
The difference is an informative error message at compile time when such fails to satisfy the 'refinement'

richard_fey 3y ago

How do you define operations on these liquid types? You can't even define subtraction or addition on this "non zero integer type". These types are not closed so how is it useful?

maxbond 3y ago
Addition isn't a problem, any nonzero integer plus a nonzero integer is a nonzero integer. For subtraction it becomes fallible. You get back an option, 5 - 4 = Some(1), 4 - 5 = None. (These are probably methods rather than infix operators, your language may vary.) See for example the methods documented here: https://doc.rust-lang.org/stable/std/num/struct.NonZeroUsize.html https://doc.rust-lang.org/stable/std/num/struct.NonZeroUsize... As for it's utility, it enables certain optimizations and it can be a useful constraint. Eg for ensuring that you don't divide or multiply by zero.
- pharmakom 3y ago
  It would be in interred ring to have a memory bounds for the program too!
- zokier 3y ago
  It is worth pointing out that the same problems apply to "normal" integer types like int32/uint32; you can trivially over/underflow the bounds with basic arithmetic. In that sense it doesn't really matter what the bounds are exactly.
- School-Cotton 3y ago
  > any nonzero integer plus a nonzero integer is a nonzero integer That’s not true. 5 + (-5) is 0.
  - maxbond 3y ago
    You're right, I was thinking of a nonzero unsigned integer. D'oh! Thanks for the correction!
saithound 3y ago

skybrian 3y ago

An important thing to remember about fancy type systems is that they can only make guarantees in a closed world. If your data comes from the network or a file, you will likely need a reader or parser that does runtime checks somewhere, but a good type system can provide assurance that you did each check exactly once. On a complicated single-process system (a monolith), that can be a big improvement. For distributed systems (microservices), there will still be plenty of runtime checks. That's what allows each service to have its own lifecycle. I'm wondering what Elixir will do, given that Erlang servers divide up work into lots of independent, distributed components?

shepherdjerred 3y ago
This is a fantastic point, and a huge issue that I had with TypeScript. Libraries for TypeScript like Zod[0] allow you to define types and validate against them at runtime. For example: https://stackblitz.com/edit/typescript-pwzng4?file=index.ts https://stackblitz.com/edit/typescript-pwzng4?file=index.ts At work, we use this to validate API responses, local storage contents, or URL/router data. It solves the problem you described -- dirty data coming from outside of the type system. This isn't a plug for Zod or TypeScript -- there are other similar libraries for TypeScript, and I would imagine other statically typed languages have something to fill this role. [0]: https://zod.dev/ https://zod.dev/
- svrtknst 3y ago
  TypeScript became so much more pleasant to use after we started using parsers regularly. We use Runtypes in some projects and a hand rolled lib I wrote in others, and being able to parse unknown data into a known shape is a life saver. Glad to not have to write seemingly thousands of lines of interfaces and type guards any more.
- diarrhea 3y ago
  Two random thoughts: - why is there `safeParse`? Why is parsing not safe by default? Have an `unsafeParse` as an escape hatch, not the other way around. - the imperative check for `success` seems unfortunate. Then again, I am familiar with pydantic from Python, which seems awfully similar to Zod, and there you'd get an Exception on failure which you'd have to catch. Some would call that uglier (I don't). Point being, I don't know of a better alternative, but sure hope native liquid/dependent types wouldn't suffer from this anymore

everybodyknows 3y ago

Title needs to append (2015).

eithed 3y ago

If Int (without 0) should be used, why not use IntWithoutZero type?

LeanderK 3y ago

I wonder how pragmatic those can become. Usually I don't really care about "exact" exactness, a common theme in haskell. A sort of "under common assumptions" (no underflow/overflow/OOM etc.) proof of laws and properties. This eliminates a whole class of bugs and strengthens your ability to reason, but doesn't make everything super, super complicated by thinking about all those edge cases. One usually doesn't program airplane control software. Some bugs are okay and speed of development and correctness is a trade-off.

mabbo 3y ago

I wonder what is possible in more common languages like Java or Python. Certainly, the language itself won't have liquid types in the compiler any time soon. But taking Ruby's Sorbet as inspiration, I wonder if you could annotate Java classes with semantic rules and do some simple verifications as a post-compilation step? There's too much bad code out there that can't just be replaced. Tools to help make it better would be a huge boon.

c-cube 3y ago
In 2008 at univ I had a few classes using http://krakatoa.lri.fr/ http://krakatoa.lri.fr/. Tools definitely exist, although you could probably argue that the production ready version of that that people use in practice is really Ada/SPARK (built on similar technologies if not the same)
sn9 3y ago
Java has JML [0] and Python has all sorts of DBC libraries that can accomplish something similar [1]. [0] https://www.thestrangeloop.com/2018/contracts-for-getting-more-programs-less-wrong.html https://www.thestrangeloop.com/2018/contracts-for-getting-mo... [1] https://www.hillelwayne.com/talks/beyond-unit-tests/ https://www.hillelwayne.com/talks/beyond-unit-tests/