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?
Jaro Reinders
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.
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`?
- Netherlands
- 4 years, assumes Master's
- 0*
- 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.
@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.
