I'll keep shilling for liquid types because I really want them to become standard...

I'll keep shilling for liquid types because I really want them to become standard. They aren't getting nearly as much hype as dependent types, but are much more practical for proving the correctness of programs directly in the type system.

Other urls found in this thread:

github.com/davidfstr/idris-insertion-sort/blob/master/InsertionSort.idr
ucsd-progsys.github.io/liquidhaskell-blog/
ucsd-progsys.github.io/liquidhaskell-blog/static/img/splash-ups.png
twitter.com/AnonBabble

Why?

Unlike dependent types, inferrable refinements don't mess up type inference. Starting from the axioms you provide, the compiler can just prove all your invariants for you using ordinary type inference.

It's an extremely easy solution to use, which adds almost no verbosity to the language. Dependent types blow up simple things like insertion sort to thousand line projects because of how verbose it is to prove the simplest things using them.

WTF that image.

>> Not writing your insertion sort in Idris.
github.com/davidfstr/idris-insertion-sort/blob/master/InsertionSort.idr

>another good name wasted for some arbitrary static check/partial evaluation
And I say that as a static everything guy.

Hopefully this is not a new language, because in that case it's probably the only good property about it what means it will be forgotten.

Pic related is an implementation as a GHC Haskell extension that uses an SMT solver as a backend during typechecking. It's fully compatible with ordinary Haskell since it's basically just a library that you install with cabal or stack.

Good on you.
Then again, Haskell suffers from the same problem.

Whatever it is, Sup Forums is probably the wrong place.

>They aren't getting nearly as much hype as dependent types
That's because they're less powerful. It shouldn't be a surprise.

arent functional languages supposed to be "easy to read"?

Brainlet procuderal programmer here. Can you explain without a """liquid type""" is for me without all the complicated math stuff and those symbols/operators from the image?

They're a lot more readable than AbstractSideEffectingExceptionThrowingGenericFactoryMethodInvokingBeanBean

No

First image says that the input is an integer greater than zero, and so is the output. The compiler notes that the n-2 case might be smaller than zero if the input is 0 or 1. The error disappears when both the zero and 1 cases are handled.

The second image has an OrdList type which is just an ordered list of items. The compiler notices that the inquality goes the wrong way in insert so that the output would not be sorted (as the type signature says), and notifies the user.

Basically, it's just an addition to the type system that lets you add a bunch of annotations to ordinary types, with conditions that the compiler should check.

>procuderal
Did you fucking do that on purpose to annoy me?

what text editor is this?

nano

Do you use them everywhere or just in safety-critical parts?
For example, I only write quickcheck properties when I want to be sure that some invariant holds, but I don't really strive for code coverage

Ideally you should use them everywhere. They impose zero runtime cost. In my view they're considerably more useful and easier to use throughout your code than unit tests.

Neat. Do you know a blog post/paper about the theoretical/practical differences between liquid and dependent types? I always sort of assumed that, since I never hear anything about LH anymore it sorta got obsoleted by DT

Do you Haskell niggers have any point other than being irrelevant? Who the fuck cares about liquid types?

Which language do you like that you believe is threatened by Haskell's existence?

you know how programming sucks? in haskell, it only sucks half as bad

None, because Haskell has no userbase.

You write me a customer ticket database on Haskell. You have 5 minutes.

Haskell artisans don't sully themselves with such common trash.

The currently most practical implementation of liquid types is in Haskell, but strong static typing is not unique to Haskell.

Procedural languages could have something similar as well. They'd probably benefit even more from it since they tend to be more subject to things like off-by-one errors.

With that said, Haskell is simpler on that front since immutability means you never have to worry about variables changing type as they are mutated, which means you have fewer details to think about when implementing it.

what's the predicate for ordered list (OrdList in the animation) look like?

The concept is actually called "refinement typing", Liquid is just an implementation of that on top of haskell:
ucsd-progsys.github.io/liquidhaskell-blog/

ucsd-progsys.github.io/liquidhaskell-blog/static/img/splash-ups.png

ucsd-progsys.github.io/liquidhaskell-blog/

Yo dawgs.

What if you gave types to types so that you can infer that a type is inferrable so that you can infer that you can infer while you are inferring?

And then restrict use of dependent types to the constructions that provably don't break type inference. I.e. enforce totality for types.

types have types, called kinds, that are inferred? and things that can be inferred still are?

This makes me curious about how easily this could be applied to rust.

AFAIK microsoft's dependently typed F* language is heavily built on this. It has full dependent types but strongly empathizes the subset which doesn't break type inference and which are effectively refinement types (liquid types). It's pretty neat.

Time ... rust team stop fap fap on safe memory

I guess that's consistent with F* being the only dependently typed language with a bootstrapped compiler.

Writing an Agda/Idris compiler in Agda/Idris is probably going to be a more or less impossible task because of their lack of expressiveness.

Thanks, user.
That's pretty neat

>fib 0 = 1
Kick that mouth-breathing retard out of here.