sgraf

sgraf, 12 days ago to random German

I'm currently evaluating what is the best hygiene system to implement in Template Haskell, because the current one is not even hygienic: https://gitlab.haskell.org/ghc/ghc/-/issues/24713

I must say, I found the literature a bit confusing for lack of succinct examples that distinguish new/concurrent systems from prior work. Good thing there is https://dl.acm.org/doi/10.1145/3386330 which at least helps me trace decisions that led to different systems and brings a few examples as well.

kha, 13 days ago to random

Omg. In Munich, even the dentist is posh as hell

joey, 24 days ago to random

Anyone have recommendations for a good ergonomic keyboard? My old Microsoft 4000 is wearing out

brokenix, 27 days ago to haskell

quoting @prophet
mli files are mostly used to constrain the visibility of definitions whereas hs-boot files are about allowing mutual recursion between modules (which OCaml doesn't support, even with mli files!)
But the mechanism by which they achieve their goals is nearly identical even though the perception of it is so vastly different.

I guess the conclusion to draw from this is that both sides are wrong: IMO, mli files are not nearly as good as OCamlers think they are, but hs-boot files aren't as ugly as Haskellers think either.
-- prettySrcLoc and prettyCallStack are defined here to avoid hs-boot
-- files. See Note [Definition of CallStack]

Backpack's design is primarily driven by compatibility considerations (“how do we build upon GHC's existing foundation?”), rather than elegance. In particular, Backpack doesn't eliminate those ugly .hs-boot files, it just automates and hides their generation and processing.

For all their faults, Standard ML and OCaml have pretty good support for modular programming. And, as the Modular Type Classes paper you linked shows, type classes can be built elegantly on top of a good modular foundation.
#ocaml #haskell
https://cohost.org/prophet/post/3251638-it-s-really-interest
https://haskell.fi.muni.cz/doc/base/src/GHC-Exception.html
https://twitter.com/lexi_lambda/status/1172629363730333697
https://news.ycombinator.com/item?id=11371130

sgraf, 27 days ago to random German

This paper (or rather, the research field it provides an overview of) could have saved me a lot of head-scratching if I had known about it a year ago: https://www.cambridge.org/core/journals/journal-of-functional-programming/article/impact-of-higherorder-state-and-control-effects-on-local-relational-reasoning/DA921680527426F49ED79644C8C6A565

What is your favorite case of "Related Work that I wish I had known about before reinventing the wheel"?

zanzi, 1 month ago to random

I kinda feel like there should be a link between monadic parsers and monad comprehensions, since both are based on similar structures (MonadPlus, Alternative). Has anyone written about this?

brokenix, 1 month ago to haskell

pseq combinator is used for sequencing; informally, it eval-
uates its first argument to weak-head normal form, and then eval-
uates its second argument, returning the value of its second argu-
ment. Consider this definition of parMap:
parMap f [] = []
parMap f (x:xs) = y ‘par‘ (ys ‘pseq‘ y:ys)
where y = f x
ys = parMap f xs
The intention here is to spark the evaluation of f x, and then
evaluate parMap f xs, before returning the new list y:ys. The
programmer is hoping to express an ordering of the evaluation: first
spark y, then evaluate ys.
The obvious question is this: why not use #Haskell’s built-in seq
operator instead of pseq? The only guarantee made by seq is that
it is strict in both arguments; that is, seq a ⊥ = ⊥ and seq ⊥
a = ⊥. But this semantic property makes no operational guaran-
tee about order of evaluation. An implementation could impose this
operational guarantee on seq, but that turns out to limit the optimi-
sations that can be applied when the programmer only cares about
the semantic behaviour. Instead, we provide both pseq and seq
(with and without an order-of-evaluation guarantee), to allow the
programmer to say what she wants while leaving the compiler with
as much scope for optimisation as possible.
https://simonmar.github.io/bib/papers/multicore-ghc.pdf

anuytstt, 2 months ago to random

Yay!
https://www.cs.mcgill.ca/~bpientka/papers/esop24.pdf

jesper, 2 months ago to random

Is there anything known about the efficiency implications of using HOAS for representing the (internal) syntax of a lambda calculus instead of de Bruijn syntax? Assuming one can get away with it, it seems like it could theoretically speed things up compared to looking up things in lists. OTOH functions can do arbitrary things, so I imagine much would depend on how you actually construct these.

Maybe @AndrasKovacs has an idea?

underlap, 2 months ago to haskell

There are plenty of descriptions of Haskell's do notation as syntactic sugar for stringing together sequences of operators such as >>=.

There are also "laws" that define the semantics of the do notation.

But I haven't found any decent description of how to use do notation as if it was a first class language construct. That would be especially useful for beginners.

Anyone know of such a description?

Boosts appreciated!

#Haskell

mangoiv, 3 months ago (edited 3 months ago) to random

random stuff:
I have long ago started writing Haskell types like: newtype A = MkA {unA :: B}, to avoid punning. So far, so good. However, someone told me that writing this: f (MkA b) = ... is somewhat odd because you don't MkA, you only do that the other way around. So I have started doing this very cursed thing everywhere I have a MkA-like constructor: f (unA -> b) = ...

sgraf, 3 months ago to random German

How do people (well, semanticists) say in short terms that some syntactic restriction is necessary to "work around the lack of full abstraction" in their semantic domain?

E.g., I have some lemma f(d) <= g(f,d) that I need to prove correct, and I can only do so if I assume that f = [[λx.e]] for some e. I say "this syntactic restriction is necessary due to a lack of full abstraction", which seems very indirect.
Is there a more succinct term to describe this?

https://www.pls-lab.org/en/Full_abstraction