Skip Navigation
jaror jaror @kbin.social

All the side effects were never mentioned to me I am innocent of uncontrolled abuse

Posts 173
Comments 82

Type Theory Forall Podcast: David Christiansen

www.typetheoryforall.com Type Theory Forall

Type Theory much beyond inference rules

In this episode we talk with David Christiansen, he wrote the books Functional Programming in Lean and the Little Typer.

He has also worked as the Executive Director of the Haskell Foundation, at Galois and did his PhD developing a bunch of cool stuff for Idris.

David is a super upbeat person and I feel that we could spend hundreds of hours talking about Functional Programming Writing and Dependent Types, and we still wouldn’t run out of topics!

0

Haskell Interlude Podcast 49: Arseniy Seroka

haskell.foundation Arseniy Seroka

Wouter and Joachim interview Arseny Seroka, CEO of Serokell. Arseny got into Haskell because of a bet over Pizza, fell for it because it means fewer steps between his soul and his work, and founded Serokell because he could not get a Haskell job. He speaks about the business side of a Haskell compan...

Wouter and Joachim interview Arseny Seroka, CEO of Serokell. Arseny got into Haskell because of a bet over Pizza, fell for it because it means fewer steps between his soul and his work, and founded Serokell because he could not get a Haskell job. He speaks about the business side of a Haskell company, about the need for more sales and marketing for Haskell itself, and about the Haskell Developer Certification.

0

[Well-Typed Blog] Improvements to the ghc-debug terminal interface

ghc-debug is a debugging tool for performing precise heap analysis of Haskell programs (check out our previous post introducing it). While working on Eras Profiling, we took the opportunity to make some much needed improvements and quality of life fixes to both the ghc-debug library and the https://hackage.haskell.org/package/ghc-debug-brick terminal user interface.

To summarise,

  • ghc-debug now works seamlessly with profiled executables.
  • The ghc-debug-brick UI has been redesigned around a composable, filter based workflow.
  • Cost centers and other profiling metadata can now be inspected using both the library interface and the TUI.
  • More analysis modes have been integrated into the terminal interface such as the 2-level profile.

This post explores the changes and the new possibilities for inspecting the heap of Haskell processes that they enable. These changes are available by using the 0.6.0.0 version of https://hackage.haskell.org/package/ghc-debug-stub and https://hackage.haskell.org/package/ghc-debug-brick-0.6.0.0.

0
discourse.haskell.org Bluefin, a new effect system

I’ve mentioned my new effect system, Bluefin, a few times on this forum. It’s now ready for me to announce it more formally. Bluefin’s API is differs from all prior effect systems in that it implements a “well typed Handle/Services pattern”. That is, all effects are accessed through value-level han...

Bluefin, a new effect system

I've mentioned my new effect system, Bluefin, a few times on this forum. It's now ready for me to announce it more formally.

Bluefin's API is differs from all prior effect systems in that it implements a "well typed Handle/Services pattern". That is, all effects are accessed through value-level handles, which makes it trivial to mix a wide variety of effects, including:

If you're interested then read the Introduction to Bluefin. I'd love to know what you all think.

0

[Well-Typed Blog] Choreographing a dance with the GHC specializer (Part 1)

well-typed.com Choreographing a dance with the GHC specializer (Part 1)

This is the first of a two-part series of blog posts on GHC specialization, an optimization technique used by GHC to eliminate the performance overhead of ad-hoc polymorphism and enable other powerful optimizations. There will also be a Haskell Unfolder episode about this topic.

Choreographing a dance with the GHC specializer (Part 1)
0

Haskell Interlude 46: effectfully

haskell.foundation effectfully

Roman, known better online as effectfully, is interviewed by Wouter and Joachim. On his path to becoming a Plutus language developer at IOG, he learned English to read Software Foundations, has encountered many spaceleaks, and used Haskell to prevent robots from killing people.

Roman, known better online as effectfully, is interviewed by Wouter and Joachim. On his path to becoming a Plutus language developer at IOG, he learned English to read Software Foundations, has encountered many spaceleaks, and used Haskell to prevent robots from killing people.

0
Simple Programming Languages
  • The machine itself can generally only do very simple things

    I disagree. Assembly languages for modern architectures are a complexity hell. You need books with thousands of pages to explain how they work. In comparison the lambda calculus is much simpler.

  • well-typed.com The Haskell Unfolder Episode 22: foldr-build fusion

    When composing several list-processing functions, GHC employs an optimisation called foldr-build fusion. Fusion combines functions in such a way that any intermediate lists can often be eliminated completely. In this episode, we will look at how this optimisation works, and at how it is implemented ...

    The Haskell Unfolder Episode 22: foldr-build fusion
    0

    Haskell Interlude 45 - András Kovács

    haskell.foundation András Kovács

    In this episode, András Kovács is being interviewed by Andres Löh and Matthias Pall Gissurarson. We learn how to go from economics to functional programming, how GHC's runtime system is superior to Rust's, the importance of looking at GHC's Core for spotting stray closures, and why staging might be ...

    In this episode, András Kovács is being interviewed by Andres Löh and Matthias Pall Gissurarson. We learn how to go from economics to functional programming, how GHC's runtime system is superior to Rust's, the importance of looking at GHC's Core for spotting stray closures, and why staging might be the answer to all your optimisation problems.

    0
    RE: Is Ernest still here?
  • AP probably stands for ActivityPub

  • Haskell Interlude 44: José Manuel Calderón Trilla
  • That's odd. This latest episode is indeed not mentioned on there: https://feeds.buzzsprout.com/1817535.rss. I'd guess it is something on buzzsprout's side.

  • The Pure Programming Language (2022)
  • The symbolic rewriting is interesting.

    I do wonder what "modern-style" functional programming means.

    Also their FAQ says:

    But considering other FPLs like Haskell and ML, Pure's library support isn't bad

    Clicking that link reveals a list of about 34 libraries. In comparison, Haskell's current curated Stackage snapshot has 3340 packages in it (the total number of packages is probably more than 10x that). So, I think it is odd to claim its ecosystem is anywhere near Haskell's.

  • I enjoyed the simplicity of this recent Computerphile video on web servers: [https://www.youtube.com/watch?v=7GBlCinu9yg](https://www.youtube.com/watch?v=7GBlCinu9yg)
  • We can make it a lot more performant, shorter, and also safer by using lazy byte strings:

    {- cabal:
    build-depends: base, network, network-run, bytestring
    -}
    
    {-# LANGUAGE OverloadedStrings #-}
    
    import Network.Run.TCP (runTCPServer)
    import qualified Network.Socket.ByteString.Lazy as Net
    import qualified Data.ByteString.Lazy.Char8 as Str
    
    main = runTCPServer (Just "127.0.0.1") "9999" $ \s -> do
      request <- Net.getContents s
      case Str.words (Str.takeWhile (/= '\r') request) of
        ["GET", resource, "HTTP/1.1"] -> do
          let path = Str.concat
                [ "htdocs/"
                , Str.dropWhile (== '/') resource
                , if Str.last resource == '/' then "index.html" else ""
                ]
          page <- Str.readFile (Str.unpack path)
          Net.sendAll s ("HTTP/1.1 200 OK\r\n\r\n" <> page)
        _ -> error "todo"
    
    
  • I enjoyed the simplicity of this recent Computerphile video on web servers: [https://www.youtube.com/watch?v=7GBlCinu9yg](https://www.youtube.com/watch?v=7GBlCinu9yg)
  • Actually, if you combine network with network-run then it is the right level of abstraction:

    {- cabal:
    build-depends: base, network, network-run, monad-loops
    -}
    
    import Network.Run.TCP
    import Network.Socket
    import System.IO
    import Control.Monad.Loops
    
    main = runTCPServer (Just "127.0.0.1") "9999" talk where
      talk s = do
        h <- socketToHandle s ReadWriteMode
        l <- hGetLine h
        case words l of
          ["GET", resource, "HTTP/1.1"] -> do
            whileM_ (("\r" /=) <$> hGetLine h) (pure ())
            let path = concat
                  [ "htdocs/"
                  , dropWhile (== '/') resource
                  , if last resource == '/' then "index.html" else ""
                  ]
            hPutStr h "HTTP/1.1 200 OK\r\n\r\n"
            hPutStr h =<< readFile path
            hClose h
          _ -> error "todo"
    
    
  • Haskell's problem with exploding call stacks
  • Another way to put it is that HasCallStack isn't optimized away by tail call optimization. And Haskell without tail call optimization will have huge stacks.

  • Haskell Interlude 41: Mike Angermann
  • The discussion about incentives for stability was interesting. It reminded me of the maintainership standards proposal. I think it would be very useful to have Hackage show information like how quickly a package fixes version bounds when new versions of their dependencies are released.

  • Well-Typed Blog: Haskell Symposium 2023
  • @kosmikus @mangoiv I'm not really the right person to ask, having spent exactly zero time in industry. But I can imagine most industrial users have little interest in the main ICFP program and the other co-hosted workshops. So hosting the event separately at a smaller venue for just two days could make it possible to substantially lower the fees (and individual accommodation costs) which naturally makes the event more accessible. And I expect that the fees are generally a bigger problem outside of academia, so it cater more to industrial users and hobbyists.

  • [Well-Typed] The Haskell Unfolder Episode 17: circular programs
  • This was a fun episode. I was introduced to breadth first labeling and attribute grammars by Doaitse Swierstra at the Applied Functional Programming summer school in Utrecht. He was an inspiring figure.

    The biggest disadvantage of circular programs is that it is very easy to get into infinite loops when you make mistakes. I wish there was an easy way to guarantee statically that circular programs are terminating (perhaps using types).

    There is also a recent paper about implementing breadth-first traversals without relying on laziness: https://www.cs.ox.ac.uk/people/jeremy.gibbons/publications/traversals.pdf. Unfortunately, that does not contain any benchmarks.

  • Well-Typed Blog: Haskell Symposium 2023
  • Maybe the symposium should start catering more to industrial users, now that Haskell itself also seems to be moving more in that direction (e.g. more backwards compatibility). The symposium already allows experience reports and demos.

  • The Haskell Unfolder Episode 16: monads and deriving via
  • For more details on DerivingVia, check out the paper:

    https://ryanglscott.github.io/papers/deriving-via.pdf

    Especially Section 4 which lists many use cases including the superclasses demonstrated in the video.

  • Haskell Interlude 38: Edwin Brady
  • I think Idris' bang notation for performing effects in a do-block is pretty, it could look like this:

    main = do putStrLn ("You said: " ++ !getLine)
    
    

    Today, you'd have to come up with a new variable name or figure out the right combinator names:

    main = do line <- getLine; putStrLn ("You said: " ++ line)
    
    main = putStrLn . ("You said: " ++) =<< getLine
    
    

    But unfortunately there are more complicated cases:

    main = do print (True || !getLine == "foo")
    
    

    In a strict language with built-in short-circuiting logical operations the getLine would never be performed, but in Haskell || is just a normal function that happens to be lazy in its second argument. The only reasonable way to implement it seems to be to treat every function as if it was strict and always perform the getLine:

    main = do line <- getLine; print (True || line == "foo")
    
    

    Do you think this is confusing? Or is the bang notation useful enough that you can live with these odd cases? I'm not very happy with this naive desugaring.

  • GHC proposal: Linear constraints
  • The changes seem pretty modest as the costs and drawbacks section also says. But I wouldn't know how complicated it is to combine normal constraints with dependent types, let alone linear constraints.