Process journal of learning by Attila Vajda

Google Summer of Code 2026

Google Summer of Code 2026 my xp #

my anecdotes, and experience of... at the I don't know how to start this blog, or do I, after all I have already started writing it as I am writing it now... uhm GSoC, I decided to try it, and chose Haskell idea Liquid Haskell

My experience was, uhm, I chose it because, I was looking for an abstract mathematics, structural something I care about

It's awesome, I believe it is awesome to do this GSoC so I encourage you to look at ideas or propose your own and get in touch with mentors, if this something that you care about, maybe it turns out to be meaningful.

functions are constructive proofs! 🎉 #maybe #

so I thought I write this blogpost, because the GSoC project mentions a blogpost as an outcome I don't even know yet how do you become the contributor to one of these projects, but I have a few maybe meaningful ideas so I am doing those

- functions are constructive proofs! 🎉 #maybe is something interesting I just learned while learning the code for the Liquid Haskell Plugin.hs

I noticed it is as if it is a sort of different language for the same patterns you are already familiar with.

It's done, the blogpost is written. Imperfect, an mvp, and there you go. 🎉

different language same patterns? #

sort of the same #perhaps typeclass, refinement, Core, are new words I learnt

a monad is 2-monoid? #

there are many of these insights and learnings that I find delighting, so I thought it would make sense, in other words it would be meaningful to share those. So I thought the concept of monoid is already somewhat familiar for me, and looked up monad in Categories [Mac Lane] and learnt a monad is a

now a question I have which seems interesting in my experience is monad seems to be used in Haskell as a function, with input and output, so monoids have inputs and outputs also, and then things like the natural numbers have input and output? (I mean, I can sort of see a number as an arrow already, but the entire whole lot of ℕ, like, what do you input and what does it output?) I guess everything can be seen as an arrow in mathematics, because for example if you have as your foundations arrow-only formulation of categories and build logic and everything out of nothing but arrows then maybe everything you ever have is arrows. Maybe this is induction? It seems like induction to me,

plugin :: GHC.Plugin #

plugin :: GHC.Plugin

Is this p:G or x:A? Π or ∑? Π (x : Module) ∀x:A Π_(x:A) λx.b? x : A est le point d'entrée ?⛵️✨ le mappe → Noyau vérifié un morphisme agissant sur un objet de la catégorie

Closure seems related, which was surprising for me, a new connection, I learning something. closed ~ scoped ~ no free variables LH maybe sort of makes sure structure is preserved, maybe it is LH preserves structure. Something for me very interesting is that homology and homotopy theory are functors! It's similar to the idea where a monad is a sort of function with input output, and a monoid is also, and so if a theory is also a functor then a theory is also a sort of function with input output. Then is the real number system ℝ again a sort of function with input output? Is the real number system a theory? Is Haskell a theory and a functor and a sort of function?

LH préserve la structure types, raffinements, morphismes de base

If mathematics is the theory of analogy, then is analogy a functor? 🤖🌿 Si les mathématiques sont la théorie de l'analogie, alors une analogie applique des structures → des structures préservant les relations.

Are there patterns of HoTT in LH? #

I wonder

plugin = GHC.defaultPlugin { … }

C a ⟹ Dict_C a #

instance→dict term

class C (α) := (op : α→α)
def use [C α] (x:α) := C.op x
-- elaborates: use (d: C α) x

use :: C a => a->a
-- Core: use d x