Elektrine
Log in Register
Paige Chat Timeline Gallery Friends Email Drive DNS Private DNS Domains VPN Kairo Nerve
Remote

Jaro Reinders

@jaror@social.edu.nl
mastodon 4.7.3
  • Open on social.edu.nl

PhD student at Delft University of Technology 🎓 in the @DelftPL@akademienl.social group. Trying to build correct compilers from modular building blocks 🧩 in #Agda.

I'm also a #Haskell enthusiast, #GHC contributor, and a member of the GHC Steering Committee and the Core Libraries Committee.

Other than that, I like to play #folk guitar 🎶 and practicing a bit on my banjo 🪕. I also appreciate playing with language 📝 #lightverse.

120 Followers
125 Following
15 Posts
Joined February 25, 2023
Codeberg:
https://codeberg.org/jaror
homepage:
https://jaror.nl (WIP)
orcid:
https://orcid.org/0000-0002-6837-3757
Open post
Jaro Reinders @jaror@social.edu.nl
· 5mo ago

The discussion on the use of AI in the Agda project last week has convinced me I need to do more to push back against its use in projects I contribute to. However, I alone do not have the power to change the policy of all projects I want to contribute to over night. Are any groups organizing against AI in open source? Do you think that could be effective? Would you join?

16
2
11
1
Open post
Jaro Reinders @jaror@social.edu.nl
· 5mo ago
Replying to
@helge@mastodon.social @jonmsterling@mathstodon.xyz @de_Jong_Tom@mathstodon.xyz @ionica@mathstodon.xyz fun fact: the Dutch word for maths, wiskunde, is so different from most other languages because of one 17th century guy called Simon Stevin inventing cool new names for all the sciences.
5
2
0
0
Open post
Jaro Reinders @jaror@social.edu.nl
· 2mo ago
Replying to on social.vivaldi.net
@everton137@social.vivaldi.net @Fairphone@social.weho.st I also had a bad experience with the Fairbuds. For me the biggest problems were that they would occasionally shut down and the latency when watching video. Also, if I went running with one bud it would shut down every 5 minutes. Some of these issues were confirmed to be fundamental by the extremely slow Fairphone support. Now I'm much happier with the JBL Tour Pro 3. It is more expensive, but it blows the Fairbuds out of the water.
1
1
0
0
Open post
Jaro Reinders @jaror@social.edu.nl
· 6mo ago
Replying to
@kottke if only all software was required to include the tools for maintenance, diagnosis, and repairs. Ever wondered why there are no third party repair shops for software? It's because almost all software is locked up like John Deere's tractors. Only the owner of the software is allowed to fix issues and it is not you.
3
0
0
0
Open post
Jaro Reinders @jaror@social.edu.nl
· 4mo ago

Problem of the day:

Derive a fused function equal to `dupLast . dupLast` where

dupLast [] = []
dupLast [x] = [x,x]
dupLast (x:xs) = x : dupLast xs

Experienced functional programmers might see at a glance what the fused function looks like, but how do we derive it formally from the definition of `dupLast`?

#haskell #functionalprogramming

social.edu.nl

SURF Mastodon

2
4
2
0
Open post
Jaro Reinders @jaror@social.edu.nl
· 3mo ago
Replying to
@jer_gib@functional.cafe I like category theory as much as the next Haskeller, but I really can't fault anyone for thinking the applications sound underwhelming compared to all the theory from the rest of the book they'd have to learn first. Is it a didactic choice to focus more on the theory, or do you think the theory itself is not developed enough to fully explain programs like the game snake, a sudoku solver, a text editor, a web server, etc.?
1
1
0
0
Open post
Jaro Reinders @jaror@social.edu.nl
· 6mo ago
Replying to

@foxy

  1. Netherlands
  2. 4 years, assumes Master's
  3. 0*
  4. 0
  • We do need 45 "graduate school credits". These are split into: 15 credits for things like writing and presentation courses where 1 credit is basically a full day course with some homework, 15 credits for summer schools where 1 credit is one day of a summer school, and 15 "learning on the job" credits which you get for supervising students, giving a guest lecture, writing a paper, etc.
2
1
0
0
Open post
Jaro Reinders @jaror@social.edu.nl
· 7mo ago
Replying to
@slamr@hub.uckermark.social Fairphone has partnered with #murena (https://murena.com) You can buy a Fairphone with a privacy respecting alternative OS from them.
Murena - deGoogled phones and services
2
0
0
0
Open post
Jaro Reinders @jaror@social.edu.nl
· 5mo ago
Replying to
@Techaltar@mas.to Happy user of my #Fairphone 3 here (with #eOS). I feel like the recent Android updates add a lot less value than they used to, so I'm not annoyed by lagging behind. What worries me more is my power button not always unlocking immediately and my battery does not always make it through the day any more.
1
0
0
0
Open post
Jaro Reinders @jaror@social.edu.nl
· 5mo ago
Replying to
@marcosh@functional.cafe Open source AI sounds like a laudable goal, though I haven't read those proposals in detail. I'm currently mainly opposed to the use of "frontier" models which seem to be the only useful models but also definitely trained unethically (among other things). Building tools to detect AI usage is one thing, but I think it is more important to educate people about the harms of AI and show that a large group of contributors is against it.
1
0
0
0
Open post
Jaro Reinders @jaror@social.edu.nl
· 9mo ago
Replying to

@jesper @anuytstt I'm lost at this sentence in the introduction:

For example the parametricity of a function f : A → B is a proof that f maps related inputs in A to related outputs in B, i.e. f is a morphism of reflexive graphs.

Which relations on A and B are we talking about?

0
4
0
0
Open post
Jaro Reinders @jaror@social.edu.nl
· 11mo ago
Replying to
@jonmsterling I'm out of the loop on this one. What's wrong with pure type systems? Is it that it presents a general framework while only a few instantiations are really interesting (and perhaps it does not cover all interesting systems)?
0
2
0
0
Open post
Jaro Reinders @jaror@social.edu.nl
· 5mo ago

Is there any appetite to change tuple section notation in #haskell?

Here's my proposal:

https://github.com/ghc-proposals/ghc-proposals/issues/754

social.edu.nl

SURF Mastodon

0
3
0
0
Open post
Jaro Reinders @jaror@social.edu.nl
· 1mo ago

How can it be that agda.sty is causing problems for publications at #TyDe? Surely there have been literate #Agda papers published there before?

social.edu.nl

SURF Mastodon

0
1
0
0
Open post
Jaro Reinders @jaror@social.edu.nl
· 6mo ago
Replying to

@gvwilson@mastodon.social In functional programming you can abstract over patterns like that. For example, the foldMap function traverses a structure and collects all the elements according to some given mapping function and the monoid structure on the result, like how you'd use a gatherer variable in imperative languages.

Another thing that comes to mind are effect systems. The Writer effect is much lik a gatherer variable, for example. If you can define custom effects, you can separate uses of mutation.

0
0
0
0
Back
313k7r1n3
Elektrine

Tor hidden service

elekhj7afj4qnrr4yd3bkzslsyo5jgfxw3orgjkhlcxifueodybyiiad.onion

I2P eepsite

j6b6cyk6gjmepjih7jjadxgxvvf3lzzujljuu2v4biemzpg3naya.b32.i2p

Platform

  • Email
  • Chat
  • Timeline
  • VPN
  • DNS

Company

  • About
  • Contact
  • FAQ
  • Lite (no JS)

Legal

  • Terms of Service
  • Privacy Policy
  • Transparency Report
  • Report Abuse
  • Warrant Canary
  • VPN Policy

Support

  • support@elektrine.com
  • Report Security Issue
Mail client setup IMAP mail.elektrine.com:993 POP3 mail.elektrine.com:995 SMTP mail.elektrine.com:465
© 2026 Elektrine. All rights reserved. Server: 16:24:52 UTC