May 2017 - Haskell-Cafe

natVal straight to Word#
by Timotej Tomandl 13 May '17

13 May '17

Hi, I am using type-level naturals constrained to be at max the size of Word#, as such I have found myself casting the type-level naturals first to Integer and then to Word# like this type MaxConstraint a=a<=MaxNat toNatural :: forall n. (MaxConstraint n,KnownNat n)=>Natural n toNatural = Natural (integerToWord (natVal (Proxy :: Proxy n))) where MaxNat is the hard-coded value of maxBound :: Word for now, type MaxNat=18446744073709551615 My data type and the constrained constructor for Natural are data Natural (x::Nat) where Natural :: (MaxConstraint x)=>{-# UNPACK #-} !Word# -> Natural x I have tried to eliminate the integerToWord cast from toNatural, yet I have failed at doing so. As such I would like to ask, if anyone has some insight, whether it is possible to eliminate this one step of indirection. The only option I came up with is writing GHC plugin to do this. Timo

4 3

Re: [Haskell-cafe] [ghc-proposals/cafe] Partially applied type families
by Anthony Clayden 13 May '17

13 May '17

> On Sat May 13 06:40:47 UTC 2017, mniip wrote3: >> On Fri, May 12, 2017 at 01:22:35PM -0400, Richard Eisenberg wrote: >> >> My interpretation of mniips use of this descriptor was .. > That is very much correct, but what I was exactly referring to was not > the necessary limitations of type families (such as inability of partial > application) but rather their unnecessary limitations. For example only > being able to pattern-match at the top-level, or, with > InjectiveTypeFamilies, lack of 'result arg1 -> arg2' type injectivity. Don't we get limited injectivity through type family calls appearing in Equality constraints? > class (F a b ~ c) => C a b c We might have: > type instance F Int b = b And a use site which gives (a ~ Int). Then we can improve via (b ~ c). >> I agree that closed type families are bizarre and perhaps a misfeature >> -- though I think they are a good incremental step toward something better. > Closed type families have proven very useful to me, ... Thanks mniip. Yes useful to me too. (As a major user of HList-alikes.) > so I don't agree with calling them a misfeature, ... I think there were plenty of people suggesting other ways to achieve the same end. If "something better" comes out of the experience, we've lost 7~8 years of opportunity. > however I can see where you're coming from : > throughout the entire language we enforce the notion that we > can't have a "proof of type inequality" and then > closed type families give us just that. I don't like calling it "type inequality". It's proof of non-unifiability. And the rules for that are easy to write down. (Admittedly a bit messy to apply in practice.) The key fact is that Oleg et al demonstrated how it worked way back in 2004. And it works in Hugs! I don't see what's so hard. > Indeed, their semantics could be made more apparent. Disequality guards make it blimmin obvious. As described in Sulzmann & Stuckey 2002. AntC

1 0

Re: [Haskell-cafe] [ghc-proposals/cafe] Partially applied type families
by Anthony Clayden 13 May '17

13 May '17

> On Fri May 12 17:22:35 UTC 2017, Richard Eisenberg wrote: > > > On May 12, 2017, at 6:46 AM, Anthony Clayden wrote: > > So please explain here in what way > > type families are "half baked". > > My interpretation of mniip's use of this descriptor was > a reference to the fact that type families aren't just > functions, don't support `case`, ... ?? But the instance mechanism is in effect case; only considerably more powerful: > I agree that closed type families are bizarre and perhaps > a misfeature -- though I think they are a good incremental > step toward something better. What would be far better is > if we could just use `case`, and then the closed type > family syntax would desugar into case statements, much > like how normal functions work. So > > type family F a b where > F Int b = b > F a Bool = a > > (AntC's example) would really mean > > type F a b = case a of > Int -> b > _ -> case b of > Bool -> a > _ -> F a b > But this is terrible for type improvement!: It insists on working through the args left to right. And through the equations top to bottom. Contrast all the good work Richard did for closed families, to 'look ahead', detect confluence of equations, and try to make progress in solving equations. As described here https://typesandkinds.wordpress.com/2013/04/29/coincident-overlap-in-type-f… and in the 2013 paper. i.e. to mimic the behaviour of stand-alone instances. > We understand the semantics of case expressions, ... At the term level yes. But that semantics is not appropriate at the type level. Type-level programming is somewhat like term level; but quite a lot different. At the term level, we never expect to 'improve' an argument from knowledge of the result. So expecting them to behave the same, or deliberately hobbling type improvement to be like term-level case expressions is just not ergonomic. What's so difficult to understand about instances? The worst mis-feature for me about closed families, is I have to put all the instances together, not alongside the corresponding class instances -- even as associated types. 'Grounding' type instances with methods, and therefore with class instances seems to be a Good Thing, according to these musings https://typesandkinds.wordpress.com/2015/09/09/what-are-type-families/ Closed families aren't extensible when I declare a new type. The part of the (class) instance mechanism that's difficult to reason about is overlaps. So the idea of the (dis)equality guards on instances -- which can apply to class or type instances -- is to remove overlaps: essentially, if the heads overlap (are unifiable), the guards must disambiguate which instance to choose. I can't introduce in a different module an instance that overlaps. AntC

1 0

Re: [Haskell-cafe] [ghc-proposals/cafe] Partially applied type families
by Anthony Clayden 13 May '17

13 May '17

> 2 days ago Richard Eisenberg (and mniip) wrote: > ... > On incremental improvements / the "half-baked" nature of > type families: I agree completely. ... ["half-baked" is Richard quoting mniip] > ... the weird place of type families in the language. > It is my hope that Dependent Haskell will obviate > a lot of these concerns, allowing us to deprecate > type families as we know them > (you would just use an ordinary function in types > instead). I don't want to sidetrack the github discussion on mniip's proposal. https://github.com/ghc-proposals/ghc-proposals/pull/52 So please explain here in what way type families are "half baked". The part of type families I find hard to use and hard to reason about is closed type families. I'd be very happy to deprecate them, if there was something that did overlaps better. >From what I can make out, though, in Richard's Dissertation, they can't be promoted to "ordinary functions in types". If the closed equations were ordinary functions in types, you could go: > type family F a b > type instance F Int b = b > type instance F a Bool | a /~ Int = a > -- non-unifiability guard With no need for a closed sequence of choices. Is this the "case-like computations" others talk about on the proposal? AntC

3 2

Re: [Haskell-cafe] Fast JSON validation - reducing allocations
by Ben Gamari 12 May '17

12 May '17

David Turner <dave.c.turner(a)gmail.com> writes: > Ben, Eric, thanks for your help. A whole new world of low-level statistics > opens up before me... > No worries! > You're not wrong. > > I've trawled through the STG as best as I can for a newbie. The function > with a large number in the 'Alloc' column looks pretty much to be the heart > of the `step` function. There's a lot of nesting but it looks largely to be > just checking the bounds on array indices, which I don't think allocates > anything. > Something that I should have mentioned earlier is that STG has the nice property that all allocation is syntactically obvious: allocated closures manifest as `let`s. This makes it fairly easy to pick out possible allocation sites, even in large dumps. > However I see this this little snippet at the very bottom of the nesting: > > case > indexArray# [ds1_sl1b > y2_sl5H] > of > _ [Occ=Dead] > { (##) ipv8_sl60 [Occ=Once!] -> > case > ipv8_sl60 > of > _ [Occ=Dead] > { GHC.Word.W8# dt6_sl62 [Occ=Once] -> > case > ss_sl5v > of > dt7_sl63 > { __DEFAULT -> > (#,,#) [__word 1 > dt6_sl62 > dt7_sl63]; > }; > }; > }; > > > I'm guessing that the `indexArray` call is the line that reads `nextState = > aTransitionsTable makeAutomaton AU.! (currentState, nextByte)`, and to me > it looks like it might be unboxing the thing it's getting out of the array. > Not sure that counts as an allocation, but I'm surprised anyway. > The unboxing should just involve looking at the value field of the W8# closure (e.g. a memory dereference) and putting the value in a machine register. There is no allocation here as far as I can see. > I'll keep digging anyway, but it'd be good to hear of any progress at your > end too. Hope it didn't spoil your lunch! Far from it! It was nice to have a puzzle to ponder. Cheers, - Ben

4 10

Re: [Haskell-cafe] Fast JSON validation - reducing allocations
by David Turner 11 May '17

11 May '17

Ben, Eric, thanks for your help. A whole new world of low-level statistics opens up before me... On 11 May 2017 at 18:57, Ben Gamari <ben(a)smart-cactus.org> wrote: > Eric Seidel <eric(a)seidel.io> writes: > > > On Thu, May 11, 2017, at 09:12, David Turner wrote: > >> Could anyone help, e.g. by pointing me at the bit in the Core that is > >> allocating within the main loop? > > > > GHC has a -ticky flag that tracks precisely where allocations are > > happening. It's quite low level (you may have to stare at the STG in > > addition to the Core to interpret the results) but I've found it > > incredibly useful when trying to understand performance swings in GHC's > > own benchmarks. > > > > https://ghc.haskell.org/trac/ghc/wiki/Debugging/TickyTicky > > > > You can enable it per module, which is nice break from the > > rebuild-the-world -prof, but the flip side IIRC is that if the > > allocations are happening in a module that wasn't compiled with -ticky > > (e.g. somewhere inside Data.Array) you might not see them. > > Indeed, -ticky is wonderful for this sort of thing since it doesn't > affect Core-to-Core optimization, meaning that the instrumented program > will behave very similarly to the uninstrumented version (just a bit > slower due to counter overhead). > > I had a quick look at your example over lunch. I started like this > (after commenting out the aeson benchmark in Main), > > $ ghc app/Main.hs -isrc -O2 -ddump-stg -fforce-recomp \ > -ddump-to-file -dsuppress-idinfo -ddump-simpl -rtsopts \ > -ticky -ticky-allocd > $ app/Main +RTS -rticky.out Ok, I was just about to ask about the Alloc'd column as mine was all zeroes, but the -ticky-allocd was what I needed, thanks. > The table suggests a few nice starting points: $w$j1_slJT is allocated > quite a bit, probably by $wgo7_slHA. Next we can turn to the STG output > (src/Automaton.dump-stg) to try to understand why this is. Reading STG > generally tends to be quite hard due to the rather large, deeply nested > trees that most programs compile to. You're not wrong. I've trawled through the STG as best as I can for a newbie. The function with a large number in the 'Alloc' column looks pretty much to be the heart of the `step` function. There's a lot of nesting but it looks largely to be just checking the bounds on array indices, which I don't think allocates anything. However I see this this little snippet at the very bottom of the nesting: case indexArray# [ds1_sl1b y2_sl5H] of _ [Occ=Dead] { (##) ipv8_sl60 [Occ=Once!] -> case ipv8_sl60 of _ [Occ=Dead] { GHC.Word.W8# dt6_sl62 [Occ=Once] -> case ss_sl5v of dt7_sl63 { __DEFAULT -> (#,,#) [__word 1 dt6_sl62 dt7_sl63]; }; }; }; I'm guessing that the `indexArray` call is the line that reads `nextState = aTransitionsTable makeAutomaton AU.! (currentState, nextByte)`, and to me it looks like it might be unboxing the thing it's getting out of the array. Not sure that counts as an allocation, but I'm surprised anyway. I'll keep digging anyway, but it'd be good to hear of any progress at your end too. Hope it didn't spoil your lunch! Cheers, > While turning this over in my head I realized that this is the sort of > program which may be helped significantly by GHC 8.2's improved join > point handling. Indeed the timings seem to support this hypothesis: > > GHC 8.0.2 > > benchmarking json-validator/Automaton/testEvent > time 22.84 μs (22.76 μs .. 22.94 μs) > 1.000 R² (1.000 R² .. 1.000 R²) > mean 22.84 μs (22.76 μs .. 22.94 μs) > std dev 297.4 ns (221.8 ns .. 378.8 ns) > > Alloc rate 4,015,256,078,038 bytes per MUT second > > GHC 8.2 > > benchmarking json-validator/Automaton/testEvent > time 9.221 μs (9.141 μs .. 9.318 μs) > 0.998 R² (0.996 R² .. 1.000 R²) > mean 9.163 μs (9.084 μs .. 9.356 μs) > std dev 399.8 ns (193.0 ns .. 745.4 ns) > variance introduced by outliers: 54% (severely inflated) > > Alloc rate 123,141,635 bytes per MUT second > > > Wow! I suspect your allocations have now vanished. Ooo, that's more like it. Could you run again using the following to get Criterion's estimate of the allocations-per-call? json-validator-exe --regress allocated:iters +RTS -T Cheers, David On 11 May 2017 at 19:45, David Turner <dave.c.turner(a)gmail.com> wrote: > On 11 May 2017 at 19:40, Ben Gamari <ben(a)smart-cactus.org> wrote: > >> Ccing Luke Maurer under the assumption that he will appreciate seeing >> the fruits of his labor. >> >> >> David Turner <dct25-561bs(a)mythic-beasts.com> writes: >> >> > Dear Café, >> > >> (snip) >> > >> > There's a copy of the relevant code for option 4 at >> > https://github.com/DaveCTurner/json-validator. I've hacked around with >> it a >> > bit since producing the numbers above, so it's now apparently a bit >> slower >> > than Aeson but allocates less too (~65kB). >> > >> > Could anyone help, e.g. by pointing me at the bit in the Core that is >> > allocating within the main loop? >> > >> While turning this over in my head I realized that this is the sort of >> program which may be helped significantly by GHC 8.2's improved join >> point handling. Indeed the timings seem to support this hypothesis: >> >> GHC 8.0.2 >> >> benchmarking json-validator/Automaton/testEvent >> time 22.84 μs (22.76 μs .. 22.94 μs) >> 1.000 R² (1.000 R² .. 1.000 R²) >> mean 22.84 μs (22.76 μs .. 22.94 μs) >> std dev 297.4 ns (221.8 ns .. 378.8 ns) >> >> Alloc rate 4,015,256,078,038 bytes per MUT second >> >> GHC 8.2 >> >> benchmarking json-validator/Automaton/testEvent >> time 9.221 μs (9.141 μs .. 9.318 μs) >> 0.998 R² (0.996 R² .. 1.000 R²) >> mean 9.163 μs (9.084 μs .. 9.356 μs) >> std dev 399.8 ns (193.0 ns .. 745.4 ns) >> variance introduced by outliers: 54% (severely inflated) >> >> Alloc rate 123,141,635 bytes per MUT second >> >> >> Wow! I suspect your allocations have now vanished. >> > > > Ooo, that's more like it. > > Could you run again using the following to get Criterion's estimate of the > allocations-per-call? > > json-validator-exe --regress allocated:iters +RTS -T > > Cheers, > > David > >

1 0

Fast JSON validation - reducing allocations
by David Turner 11 May '17

11 May '17

Dear Café, We have a stream of ~900byte JSON documents (lazy ByteStrings) that we would like to validate (NB not parse) as quickly as possible. We just need to check that the bytes are a syntactically valid JSON document and then pass them elsewhere; we do not care what the content is. The documents are encoded in UTF-8 and have no extraneous whitespace. We have made a number of attempts: 1. Use Aeson to parse the documents and then discard the result. This was actually pretty good: Criterion clocked it at ~30us per document. 2. A hand-written Attoparsec parser. This did quite a bit worse: ~70us per document. 3. Use Get (from the binary package), which was a bit messier as it was factored to avoid all backtracking, but managed to get down to around ~20us per document. 4. Build a table-based, Word8-labelled DFA (with a minor hack to deal with values-within-values) and run it with ByteString.Lazy.foldl'. Also around ~20us per document. We didn't pursue the Attoparsec idea any further, but the other three all allocate ~85kB per document, and this now seems to be the limiting factor for performance. In more detail, looking at the threadscope output, we see it parse 5 or 6 documents in ~150us (allocating ~500kB) and then run the GC, which takes about another 150us. The GC stats indicate that it's only copying a couple of kB of live data each time, so most of that 500kB is junk. Now 85kB per document is ~96B per byte, which is only a pointer-and-a-half. It's not entirely surprising that there's this much allocation going on each time round the loop, but we'd like to try and get rid of it. I've tried the usual strictness tricks and have peered in a mystified fashion at the output of -ddump-simpl but am none the wiser. There's a copy of the relevant code for option 4 at https://github.com/DaveCTurner/json-validator. I've hacked around with it a bit since producing the numbers above, so it's now apparently a bit slower than Aeson but allocates less too (~65kB). Could anyone help, e.g. by pointing me at the bit in the Core that is allocating within the main loop? Many thanks, David

4 6

Haskell IDE Engine users?
by Alan & Kim Zimmerman 11 May '17

11 May '17

Stupid question, but is anyone using/integrating HIE into anything at the moment? I am considering rearranging the internals to orient it toward being mainly a Language Server Protocol backend , and I want to see who would be affected. Alan

1 0

Constraining constraints
by Clinton Mead 11 May '17

11 May '17

I posted the following on stackoverflow <http://stackoverflow.com/questions/43827374/what-is-a-can-be-derived-from-c…>, but it hasn't got too much attention so I thought I'd ask here: I can write the following: {-# LANGUAGE RankNTypes #-}{-# LANGUAGE FlexibleInstances #-}{-# LANGUAGE UndecidableInstances #-}{-# LANGUAGE ConstraintKinds #-} f :: Integral a => (forall b. Num b => b) -> a f = id And all is good. Presumably GHC can derive Integral from Num so all is well. I can be a bit tricker, yet I'm still fine: class Integral x => MyIntegral xinstance Integral x => MyIntegral x class Num x => MyNum xinstance Num x => MyNum x f' :: MyIntegral a => (forall b. MyNum b => b) -> a f' = id So lets say I want to generalise this, like so: g :: c2 a => (forall b. c1 b => b) -> a g = id Now obviously this will spit the dummy, because GHC can not derive c2 from c1, as c2 is not constrained. What do I need to add to the type signature of g to say that "you can derive c2 from c1"?

3 2

Galois is hiring
by Daniel Wagner 10 May '17

10 May '17

Here's our official announcement: > Galois is hiring! We're looking for researchers, principal investigators, software engineers, and project leads, including those with expertise in functional programming, formal methods, machine learning, embedded systems, computer security, or networking. We have offices in Arlington VA, Dayton OH, and Portland OR with positions available at all locations. For more info or to submit your resume, please see our website: http://galois.com/careers <http://galois.com/careers>. Here's a few things I like about Galois [1]: * Deep technical problems. I've been involved in projects to develop a prototype voting system that gives cryptographic guarantees of privacy and correctness; to get a line of mobile phones' crypto subsystems certified; to build a tool for doing asynchronous hardware design; and to obfuscate programs in a cryptographically strong way. Every day in the break room I hear about projects my coworkers are in that are as exciting or more in terms of technical depth. * Flexibility. For example, I like variety, so I've joined up with several projects even in my short stay here, working for a few months on each; but other people like stability and prefer working full-time on a single project for long periods, and both modes are well-supported. You also get quite a lot of say over what projects you'll be working on; what you'll be doing on a given project; what technologies are most appropriate for that project's goals (I've used Haskell in some way in almost every project so far... I might be biased here); even where you get your work done on any given day (Need to work from home because there's ice on the roads, or because the cable guy said they'd be there "somewhere between 10 and midnight", or just because you want to head to a coffee shop for the ambience for the day? No problem!). * Training. Everybody here is a world-class expert, and I feel like I've learned a ton just by overhearing lunch conversations. The company also goes out of its way to support structured training. I was a complete crypto noob prior to joining, but they let me spend company time on a Coursera course so that I can at least see the blood after I've shot my own foot. Each year I've been here, everyone has also been given a week for "innovation time" that need not be spent on anything directly funded from outside; many folks spend this time getting acquainted with a new technology (or inventing one!). * Location. Portland is a medium-sized city -- just large enough to have one of everything. The weather goes a little below freezing for a few days each year and a little above body temperature for a few days each year -- which is a small price to pay for the temperate weather we get the rest of the time. Walking distance from the building we're in covers a lot of ground. If those things sound exciting to you, check out our openings at http://galois.com/careers. ~d [1] Cross-posted from reddit; apologies if this looks familiar! We're still actively looking for talented folks. https://www.reddit.com/r/haskell/comments/5r3vhz/galois_is_hiring/

1 0