January 2023 - Haskell-Cafe

Benchmarking using instruction counting
by Alexey Khudyakov 25 Jan '23

25 Jan '23

Hello! I want to announce new benchmarking framework tasty-papi[1,2] Unlike criterion, gauge or tasty-bench is uses instruction counting instead of time measurements. It should be affected by OS scheduler much less so it should be possible to run benchmarks on CI. Although not on github CI (not enough permissions) For measurements papi[3] is used. So all hardware and OS limitations are inherited from there. At least it works on linux Here is example output: > 6: OK (0.02s) > ALLOC=528 TOT_INS=3609 TOT_CYC=4981 BR_INS=907 BR_MSP=58 > 7: OK > ALLOC=864 TOT_INS=5518 TOT_CYC=5138 BR_INS=1378 BR_MSP=50 > 8: OK > ALLOC=1408 TOT_INS=8614 TOT_CYC=6515 BR_INS=2142 BR_MSP=63 For each benchmark we measure number of allocated bytes, number of instructions and cycles spent as well as number of branching instructions and branch mispredictions. Counter set could be adjusted using command line flags. This library hasn't seen much real world use. So treat measurement with care. [1] https://hackage.haskell.org/package/tasty-papi [2] https://github.com/Shimuuar/tasty-papi [3] https://icl.utk.edu/papi/ - Alexey

2 1

GHC Nightlies: how would you use them?
by David Christiansen 25 Jan '23

25 Jan '23

Dear all, I'm currently helping to assemble a set of use cases that a more convenient means of accessing GHC nightly builds would support. More details are available here: https://discourse.haskell.org/t/ghc-nightlies-how-would-you-use-them/5655 Please feel free to provide feedback on that thread or via email - I'll assemble it into a final report when the discussion seems to have died down. All the best, David

1 0

Inscrutable error message from PolyKinds (should it be in GHC202X?)
by Tom Ellis 23 Jan '23

23 Jan '23

I love the idea of GHC2021, but I've just discovered that PolyKinds, which is part of it, leads to inscrutable error messages. Firstly, a scrutable error message, without PolyKinds: {-# LANGUAGE GHC2021 #-} {-# LANGUAGE NoPolyKinds #-} -- Error: • No instance for (Foldable t) arising from a use of -- ‘length’ foo :: t a -> Int foo = length Good. I know exactly how to fix that. Now the inscrutable message: {-# LANGUAGE GHC2021 #-} -- • Couldn't match kind ‘k’ with ‘*’ -- When matching types -- t0 :: * -> * -- t :: k -> * -- Expected: t a -> Int -- Actual: t0 a0 -> Int -- ‘k’ is a rigid type variable bound by -- the type signature for: -- foo :: forall {k} (t :: k -> *) (a :: k). t a -> Int -- at /tmp/bar.hs:3:1-17 -- • In the expression: length -- In an equation for ‘foo’: foo = length -- • Relevant bindings include -- foo :: t a -> Int (bound at /tmp/bar.hs:4:1) foo :: t a -> Int foo = length What? Non-expert users will experience much puzzlement. (PolyKinds tries to generalise the kind of `a` and fails, because the use of `length` restricts it to `Type`.) Should PolyKinds really be in GHC202X? Tom

3 4

Type constraint rewrite rules
by Henning Thielemann 22 Jan '23

22 Jan '23

Has anyone thought about rewrite rules for type constraints as light-weight alternative to type-checker plugins? Rewrite rules could be n + 'Zero -> n Back (Forth a) -> a for closed type families Back and Forth, where Back is the inverse of Forth Ideally the programmer would also provide a correctness proof for the proposed rewrite, e.g. with a function that generates a data BackForthProof a = (Back (Forth a) ~ a) => BackForthProof

2 1

Foldable intercalate for Data.Text?
by Benjamin Redelings 21 Jan '23

21 Jan '23

Hi, I was looking at intercalate in Data.Text, and I see that the signature is Text -> [Text] -> Text. I'm curious why this isn't (say) Foldable f => Text -> f Text -> Text Perhaps because this would be harder to optimize? -BenRI

2 2

Anyone working on improving HPC
by Ivan Perez 21 Jan '23

21 Jan '23

Hi everyone, A while back there were a few exchanges about the state of HPC and I remember reading that someone was interested in pushing a bit for improving the tool and the reports generated. Does anyone know if that's happening and who is working on that? I forgot where I saw it and I can't find it. It could have been haskell-cafe, discord, chat, idk. Thanks, Ivan

7 6

Everything you never wanted to know about Applicative laws and more
by Alexandre Esteves 21 Jan '23

21 Jan '23

I've spent some time recently going down this particular rabbit hole. The original motivation was replacing the current formulation of Applicative laws with the Monoidal-ish one, but one thing led to the other and I ended up making a post about the various sets of laws and related free theorems: https://github.com/alexfmpe/semantic-satiation/blob/main/src/Posts/001-appl…

1 0

C++ Haskell interpreter with GADTs + Type Families + Rank-n types
by Benjamin Redelings 21 Jan '23

21 Jan '23

Hi all, I don't want to oversell this, but in case anyone is interested, I've been working on a Haskell interpreter that is written in C++. This isn't intended to compete with GHC. It doesn't generate machine code, and it is not fast. However, I had a reason to try and implement Haskell typechecking in C++. So if anyone is interested in how to write their own Haskell compiler, then this might possibly be of interest. Otherwise, probably not. So far I have: 1. Parser 2. Renamer - hacky. Infix handling is a separate pass. 3. Typechecker - standard constraints + rank n types + GADTS + type families. But no newtypes and no coercions. 4. Desugarer - the desugarer generates a language w/o type-level lambdas or coercions. 5. Optimizer - inlining, let-floating, case-of-case, etc. No SpecConstr. No Rules. 6. Translation to de-Bruijn notation prior to execution (See Sestoft 1997, "Deriving a lazy abstract machine") 7. Interpreter - a special-purpose dependency-tracking interpreter. The revelant code is here: https://github.com/bredelings/BAli-Phy/tree/master/src/computation After compiling the executable, you would run use it to run a Haskell program like this: bali-phy --run-module Main.hs Tests are in: https://github.com/bredelings/BAli-Phy/tree/master/tests/haskell -BenRI

2 3

Re: [Haskell-cafe] induction on type-level Nat
by Olaf Klinke 16 Jan '23

16 Jan '23

> Alternative approach with a GADT: > > data T n a where > End :: T 0 a > Cons :: a -> T n a -> T (n+1) a > > viewL :: T (n+1) a -> (a, T n a) > viewL (Cons x xs) = (x, xs) > > testEnd :: T 0 a -> () > testEnd End = () > > > For viewL GHC reports a missing pattern match on 'End' and for > testEnd it > reports a missing match on 'Cons'. If I add the constraint (1<=n+1) > to > Cons then the testEnd warning disappears. If I add the constraint > (1<=n+1) > to viewL, then its warning disappears, as well. So the theory of type-level nats lacks the theorem forall m n. n+m <= n :: Nat -> Nat -> Constraint The infix type operator + from GHC.TypeLits constrains n in Cons to kind Nat. So the theorem above ought to be available to the type checker. Hiromi's type-natural package has Lemmas plusLeqL and plusLeqR for this. Olaf

1 0

Re: [Haskell-cafe] [ANNOUNCE] GHC 9.6.1-alpha1 is now available
by Ben Gamari 16 Jan '23

16 Jan '23

George Colpitts <george.colpitts(a)gmail.com> writes: > Hi > > I believe llvm does not work in this alpha as 21936 is still open. Is that > correct? > Indeed we do not yet support LLVM 15 but all previous LLVM versions continue to work. We can try to fix this for the final release. > I also believe that when it does work it will require llvm 15 which will be > incompatible with earlier versions of ghc. Is that correct? > Early indications suggest that supporting LLVM 15 will require that we raise the minimum supported version to LLVM 13. Cheers, - Ben

1 0