jaror avatar

jaror

@jaror@kbin.social

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

Well-Typed Blog: Haskell Symposium 2023 (well-typed.com)

The Haskell Symposium is a two-day workshop co-located with the International Conference on Functional Programming (ICFP). In a previous blog post we discussed the Haskell Implementors’ Workshop (HIW), which is another Haskell-workshop co-located with ICFP, but unlike HIW, the Haskell Symposium is a scientific workshop with...

jaror,
jaror avatar

What's up?

Haskell Interlude 39: Rebecca Skinner (haskell.foundation)

In this episode, we are joined by Rebecca Skinner. She talks about her new book, Effective Haskell, which takes you from list manipulation to thunks to type-level programming. She also tells us about large scale industrial applications in Haskell, and how the architecture is shaped by the organization of the engineering teams.

The Haskell Unfolder Episode 16: monads and deriving via (well-typed.com)

In this episode, we'll see how deriving-via can be used to capture rules that relate type classes to each other. As a specific example, we will discuss the definition of the Monad type class: ever since this definition was changed back in 2015 in the Applicative Monad Proposal, instantiating Monad to a new datatype requires...

jaror,
jaror avatar

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.

jaror,
jaror avatar

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.

jaror,
jaror avatar

My to-watch list:

jaror, to haskell
jaror avatar

Anyone want to guess how many errors this code generates:

{-# LANGUAGE DerivingVia #-}

module T where

newtype OrdList1 a = OrdList1 [a]
  deriving (Functor, Foldable, Traversable) via []

newtype OrdList2 a = OrdList2 [a]
  deriving (Functor, Foldable, Traversable) via Maybe
jaror,
jaror avatar

@mangoiv

https://play.haskell.org/saved/m7x3AiIE

jaror,
jaror avatar

For more info see: https://discourse.haskell.org/t/derivingvias-error-messages-are-bad/8217?u=jaror

jaror,
jaror avatar

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.

BoydStephenSmithJr, to vim
@BoydStephenSmithJr@hachyderm.io avatar

Does anyone else do with without ? The main agda-vim plugin doesn't work at all. The tc-0 fork does some things, but mostly emits bytes v str errors. Last time I tried the agda-language-server, I couldn't get it to compile.

I think some tooling will let me put together this evaluate function a lot faster.

jaror,
jaror avatar

@BoydStephenSmithJr I've given in and just use evil doom Emacs. It's bearable. For me the biggest problem is the performance of Agda itself.

  • All
  • Subscribed
  • Moderated
  • Favorites
  • •
  • anitta
  • rosin
  • InstantRegret
  • ethstaker
  • DreamBathrooms
  • mdbf
  • magazineikmin
  • thenastyranch
  • Youngstown
  • GTA5RPClips
  • slotface
  • Durango
  • khanakhh
  • kavyap
  • megavids
  • everett
  • vwfavf
  • Leos
  • osvaldo12
  • cisconetworking
  • cubers
  • modclub
  • ngwrru68w68
  • tacticalgear
  • provamag3
  • normalnudes
  • tester
  • JUstTest
  • All magazines
    •