Linear types make performance more predictable
blog.tweag.io
blog.tweag.io
data S a
data R a
newCaps :: (R a ⊸ S a ⊸ IO ()) ⊸ IO ()
send :: S a ⊸ a ⊸ IO ()
receive :: R a ⊸ (a ⊸ IO ()) ⊸ IO ()
In this API, S is a send capability: it gives the ability to send a message. R is a receive capability...
See [0] for a good example of well-commented but idiomatic Haskell (a snippet from the popular Megaparsec parser library), which includes things like:
data ParsecT e s m a
ParsecT e s m a is a parser with
custom data component of error e,
stream type s, underlying monad m
and return type a.
(Strawman alert.) It is significantly more work to parse (ha) something like
ExceptT fooException (StateT fooWorldState underlyingMonad) a
ExceptT e (StateT s m) a
Of course, Edward Kmett had a story about winding up with his code telling him `i m a s t a b u`...
m >>= k = ...
> Of course, Edward Kmett had a story about winding up with his code telling him `i m a s t a b u`...
Is that an indexed lens ... parameterized over a monadic type? I'd like a link to the video/article.
> I love the use of w for comonads: the rationale is apparently that it looks like an upside-down m.
That's my understanding, yeah.
> Is that an indexed lens ... parameterized over a monadic type?
Presumably further parameterized by the focus, the source structure, the target structure, the focus again, the transformed focus, and some third structure.
> I'd like a link to the video/article.
Me too :-P I see a couple references in a google search but I'm not sure where I first heard it.
The second tells me nothing - how is this intended to be used? What scope is it intended to be used in? Why was it created? Where does it fit in the program flow?
In other words, my thesis is that if you aren't familiar with State, both State s and State fooAppStateType are fairly opaque.
In any case, most of the time one works with a specialized instance, for instance, one might have something likr
newtype AppState a =
AppState {
runAppState ::
ReaderT Config
(StateT AppState IO)
a
}
If you're trying to understand how a library works when you're not very fluent in the language, that's what the documentation is there for! Any good library (and this is an area where's lots of room for improvement) should document the types it uses and the idioms that it lends itself to, and as one accrues experience, the whole "learning to see common patterns" takes over. The great thing about a helpful compiler of the Rust/Haskell ilk is that you make fewer mistakes in between (modulo occasionally horrific error messages).
And I'm willing to vouch for this not being expert (ha) blindness - I have only recently become comfortable enough with these things to talk about them.
Because each one is used only 3 times, in the same code snippet. Having long JavaStyleNames would make the provided code harder to read, not easier. Additionally, S and R are just placeholder types for this snippet; the whole point is you're supposed to replace them with some "actual" type.
> It's almost like the Haskell community takes pride in being as obscure as possible
Production Haskell code doesn't use 1-letter names like tutorials often do. Tutorials expect you to have a non-zero attention span so you can keep track of a short name across a few lines, but I've never seen this sort of thing used for type constructors in an actual library.
People with a weakly typed/untyped background also often make the mistake of confusing specificity with obscurity; Haskellers use "obscure" terms like "Functor" not because they're trying to confuse you, but because it would be wrong to use a "simpler" term. From the Haskeller perspective, it's better to spend a bit more time learning the correct concept than to save a bit of time by using a crutch intuition that will ultimately fail you.
The best way to get a concept across is to list enough examples that the reader can do their own generalization. Just tell me the abstract rule, and I will be mystified.
In math, this is why it's important to do the problem set. But you don't get to assign homework to readers in most places; you just gotta give a lot of memorable examples in the text.
Entirely and absolutely appropriate for the setting and audience.
Single letter bindings are not common in production haskell code though there are exceptions where it's very clear using single letter binding names is clear enough and not easily confused, like this for instance:
-- | Produce @Nothing@ if the first argument is @False@; produce
-- @Just a@ if the first argument is @True@.
consMaybe :: Bool -> a -> Maybe a
consMaybe b v = guard b *> pure v
makeKey :: FormatTime t
=> t -- Formattable timestamp, usually obtained with getCurrentTime
-> Text -- AWS region, e.g: us-east-1
-> Text -- AWS service, e.g: s3
-> Text -- AWS signing key protocol, e.g: aws4_request
-> Text -- AWS secret access key
-> ScopedSigningKey
makeKey ctime region service protocol key = ScopedSigningKey scope' sigkey
where
dateStamp = formatTime defaultTimeLocale "%Y%m%d" ctime -- YYYYMMDD
scope' = Data.Text.intercalate "/" [ pack dateStamp, region, service, protocol ]
sign :: ByteArrayAccess ba => ba -> C8.ByteString -> Digest SHA256
sign k m = hmacGetDigest $ hmac k m
kDate = sign (encodeUtf8 $ "AWS4" <> key) (C8.pack dateStamp)
kRegion = sign kDate (encodeUtf8 region)
kService = sign kRegion (encodeUtf8 service)
kSigning = sign kService (encodeUtf8 protocol)
sigkey = decodeUtf8 $ convertToBase Base64 kSigningLet's see how it reads if they were?
data SendCapability a
data ReceiveCapability a
newCaps :: (ReceiveCapability a ⊸ SendCapability a ⊸ IO ()) ⊸ IO ()
send :: SendCapability a ⊸ a ⊸ IO ()
receive :: ReceiveCapability a ⊸ (a ⊸ IO ()) ⊸ IO ()
That's not to say S and R are good names in a real program - name length should track scope, and type names have pretty broad scope (global but module-constrained), so they should usually be comparatively long. `SendCap` and `RecvCap` might be a good compromise, in that context. Type variables (like the `a` here) are local to the individual type signature (and, with -XScopedTypeVariables, possibly the accompanying definition) and so should be shorter. One letter may be too extreme - `a` does a fine job conveying "whatever you care to be dealing with" but `msg` might be even better in this particular case.
I agree that a good compromise is to shorten the names as long as they are still easily understandable, exactly like `SendCap` and `RecvCap`.
In math'ish problems naming/algorithm (noise ratio) needs to be kept low, otherwise you can't read through it.
You want to elevate symbols between type/vars in reader's attention (what's happening) as opposed to being detailed in naming (which is less of a problem to recall).
It's the same in other languages, just look at SHA calculation in C or anything else - it's the same, math'ish style (and it's good).
ps. another answer may be that writing code this way uses less ink! :)
I kinda sorta remember linear logic having the option for an infinite source, and an infinite sink for things you might want to deal with. A business has an infinite number of customers, but each specific transaction needs to be handled in a very specific way. You give me a dollar, and i give you a hamburger or french fries, your choice.
A light, accessible overview of linear logic is here [2]. That has a few nice, simple examples. It's easier than the wikipedia article.
declare x (must_use);
P;
use(x)
By retrofitting Haskell with linear types, there would be another linear heap. In that heap, there is no GC - resources get freed as soon as the linearly typed value is used. On can imagine programs properly annotated with linear types that don't even need ANY GC.
This is an even bigger deal in Haskell than in most other languages because Haskell, being immutable, performs a ton of allocations. Want to update a field? Nope, but you can allocate the whole object again with just that field changed. If most of that work could be moved to a linear heap which doesn't need GC... well you get the point.
Though it is still true that a purely functional language will need to allocate more than a typical imperative language.
That said with every insertion/deletion into that same tree, there is still at least log(n) garbage produced, which currently has to be handled by the GC. Linear types would let us free that garbage up as soon as it is produced and without GC pauses.
let ones = 1 : ones in ones
EDIT: I realised I forgot to say what it actually does, in case that's not obvious. It's an infinite list of, well, ones...
repeat :: a -> [a]
repeat something = [something] ++ repeat something
print (head (repeat "hello"))
Additionally, predictable performance is about what the programmer can predict (whether you are talking about throughput or latency), and the argument is that linear types make it much easier to reason about the performance of a system, hence making it more predictable.
1) When it comes to sources of unpredictability, laziness is a way bigger problem than garbage collection
2) Assuming that by "GC" we mean "some variation on mark-and-sweep" (rather than meaning "any type of automatic memory management", which I hope is not the usage of anyone in this conversation), GC cost (in terms of CPU-time consumed) doesn't care how many allocations you've done, nor how much garbage it needs to collect. All it cares about is the size of the working set at the time that it runs. As such, all those lingering copies of the old tree nodes (etc, etc) are irrelevant. So I don't see why Haskell's additional allocations should cause GC to be any more of an overhead.
In this kind of garbage collector, time of an individual garbage collection should not depend on the amount of garbage that has been generated. However, producing more garbage should mean more frequent collections, and so more time spent in GC overall.
That said, it's worth noting that a naïve attempt to free resources ASAP can be a performance hit and sometimes mean long pauses. For instance if you find yourself no longer needing a large tree, the regular GC lets you just forget about it. Freeing the whole tree would be walking the whole tree, and the naïve approach does that synchronously. Of course there are ways around that - they add some complexity, this kind of tooling will help get them right when they're needed.
All in all, performance is complicated, there are usually tradeoffs, and this seems some great tooling.
This was also super interesting: https://www.cs.cmu.edu/~cmartens/lpnmr13-short.pdf
Though at the moment the semantics isn't entirely clear to me. For instance, in the protocol example, shouldn't the pair be using multiplicative linear conjunction? It doesn't matter so much for a function receiving two Ints, but what's the semantics for a function receiving multiple ressources?
I guess you can use an impredicative encoding, e.g.
A ⊗ B = forall C. (A ⊸ B ⊸ C) ⊸ C
I don't think Cogent would be much good for writing a compiler, actually (it doesn't natively support recursive data structures like ASTs). It's designed for OS components like file systems.
I did want to learn some more about the strengths and limitations of your tool to generate ideas for other researchers. Send an email to the address in my profile. I'll reply in a few days with some questions that people here might have.
http://programatica.cs.pdx.edu/House/
They were also doing a new systems language, Habit, before reassigned to better project. Here's that project:
HalVM and House still rely on some C for the runtime, so I think my goal would be great for them.
EDIT: Having trouble typesetting the asterisk!
--*Linear types are an extension to normal types which enable them to talk about how often and when something gets used.
-> instead of comma?
-o / linear instead of refcaps?
"linear types" are certainly not linear. They are a simple reference capability, already in usage for decades. https://en.wikipedia.org/wiki/Object-capability_model
e.g. https://tutorial.ponylang.org/capabilities/reference-capabil...
Consuming a value changes its type to enable reasoning for concurrency.
As to the claim: Sure. Not only makes a refcaps type system concurrency predictable, it also makes it decidable at compile-time, and much faster. rust could learn a lot from this to avoid locking.
Because a comma would be a very unusual notation to separate the parameter and return value of a function.
For example a function with type "a -> b -> c" is not a function taking three parameters, it's a function taking something of type a returning another function of type (b -> c). Writing that as "a, b, c" would be an extremely weird way to write that.
(a) -> b
(b) -> c
E.g. take this:
inc :: Num a => a -> a
func inc (Num a) -> Num;
This is normally written without dependent types as generic for all subtypes.
func inc (Num a) -> Num;
func inc (Integer a) -> Integer;
What Haskell calls pattern matching is if you have a single type (e.g. Maybe a) with two different constructors (in this case Just and Nothing) where "Just something" will match with a value constructed with that first constructor and Nothing with the second constructor.
Note that his isn't the only thing you have wrong, there are no values of type Num, because Num is not a type. In the expression "inc :: Num a => a -> a" the only type is a, which has a restriction namely that the type has to implement the Num typeclass. The parameters don't have a name in the type signature.
If you had chosen to separate the arguments to a function using a comma, you would have to invent new syntax to describe linearity (because you have one less comma than number of arguments). Many languages constantly invent new syntax to describe useful add-ons, until their compilers are too complex to maintain at reasonable cost. Haskell avoids this by having carefully chosen which constructs to build the language out of, instead of going for recognizability/tradition.
The "linearity" of linear types comes from the typing rules of values with a linear type: They must be used exactly once. In fact, the simple typing rules of a linear type system allows one to implement all manner of capabilities and especially capabilities for references.