I wrote a blog post about Agda Core! It's a bit long and not very polished, but I'm happy to have it finished (thanks to a long and distraction-free train ride to Swansea).
A weird thing about being 50 is that there are programming languages that I've used regularly for longer than some of the software developers I work with have been alive. I first wrote BASIC code in the 1980s. The first time I wrote an expression evaluator--a fairly standard programming puzzle or homework--was in 1990. I wrote it in Pascal for an undergraduate homework assignment. I first wrote perl in the early 1990s, when it was still perl 4.036 (5.38.2 now). I first wrote java in 1995-ish, when it was still java 1.0 (1.21 now). I first wrote scala, which I still use for most things today, in 2013-ish, when it was still scala 2.8 (3.4.0 now). At various times I've been "fluent" in 8086 assembly, BASIC, C, Pascal, perl, python, java, scala; and passable in LISP/Scheme, Prolog, old school Mathematica, (early days) Objective C, matlab/octave, and R. I've written a few lines of Fortran and more than a few lines of COBOL that I ran in a production system once. I could probably write a bit of Haskell if pressed but for some reason I really dislike its syntax so I've never been enthusiastic about learning it well. I've experimented with Clean, Flix, Curry, Unison, Factor, and Joy and learned bits and pieces of each of those. I'm trying to decide whether I should try learning Idris, Agda, and/or Lean. I'm pretty sure I'm forgetting a few languages. Bit of 6502 assembly long ago. Bit of Unix/Linux shell scripting languages (old enough to have lived and breathed tcsh before switching to bash; I use fish now mostly).
When I say passable: in graduate school I wrote a Prolog interpreter in java (including parsing source code or REPL input), within which I could run the classic examples like append or (very simple) symbolic differentiation/integration. As an undergraduate I wrote a Mathematica program to solve the word recognition problem for context-free formal languages. But I'd need some study time to be able to write these languages again.
I don't know what the hell prompted me to reminisce about programming languages. I hope it doesn't come off as a humblebrag but rather like old guy spinning yarns. I think I've been through so many because I'm never quite happy with any one of them and because I've had a varied career that started when I was pretty young.
I guess I'm also half hoping to find people on here who have similar interests so I'm going to riddle this post with hashtags:
#agda seems to compile with ghc wasm backend with just a bit of modification (remove custom setup & gitrev)! i'm not familiar with agda internals, but as long as it only involves file i/o and doesn't need to spawn processes to do real work, then in principle it shouldn't be hard to get a fully functional agda in browser working :)
We are organizing the FP Dag aka Dutch Functional Programming Day on Friday the 5th of January in Delft. People from neighboring countries are also very welcome to join!
The (soft) registration deadline is on the 22th of December (next Friday), so get your tickets soon!
Does anyone else do #Agda with #Vim without #DeprecatedPython2 ? 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.
The local season for writing MSc thesis project proposal is here and I have formulated a few ideas for students to start from. They are posted in Chalmers' "MSc thesis portal" and linked from here: https://patrikja.owlstown.net/posts/1968-msc-thesis-proposals
In short, if you want to come to Gothenburg and work with #Agda or #Haskell in relation to some of my research interests, do get in touch.
Tomorrow is already the deadline for the third edition of #WITS, the Workshop on the Implementation of Type Systems, colocated with #POPL 2024 in London. The page limit is one page, but just a single-paragraph abstract with an interesting idea for a talk is also very welcome! In particular contributors to #Haskell#OCaml#Rust#Scala#Coq#Lean#Agda#Idris#Cedille#Arend#CoolTT and even #TypeScript are warmly invited to give a talk about their experiences with implementing type systems.
@pebbe I prefer my errors at compile time instead of at runtime. I prefer Haskell because I learned it first and make use of higher-kinded types in my abstractions.
Though currently, I'm trying to build a "better" language using #GRTT as the core calculus.
(Sort of, I have some properties of an evaluator for a specific grade/mode that I want to prove preferably in [#Agda] and then build a language around that instance of GRTT.)
"Concerning computer assisted proofs, it seems to me the main obstacle is user friendliness; if you want this to become a part of the culture of mathematics, that when you submit a paper it includes a computer verification that the paper is correct -- I think this is very unlikely to become a part of the culture of mathematics, but if you want it to -- then, what you need is proof assistants that mathematicians are willing to use, so that it doesn't take 100 times as long to provide that certificate as it does to produce a paper the usual way."
I just finished the first chapter of @d_christiansen's Functional Programming in #Lean, and I gotta say, theorem provers consistently win when it comes to pure fun. And Lean has been incredibly easy to dive into, find out where things are, and start... programming with, it really just feels like (or rather, is) another functional programming language, but with all the fanciness of dependent types.
I think #Agda is by far the nicest purely at the language level (I'd probably consider Agda the prettiest language after Scheme), but 2gb is a lot of space, especially for someone like me that has lots of large 3D scene files, with massive textures, and am constantly making space on my laptop. #Coq is smaller then Lean, but a lot of OCaml also bleeds through, which is a great language, but not the most elegant, and I'm just trying to grill.
#Idris is really great and the one I've spent the most time with; I was even split between diving deep into either Idris or #Scheme a few years ago and chose the latter, as Edwin Brady's book is one of the best general introductions to FP I have read. But what I'm ultimately interested in exploring is Lean's hygienic macro system, and I'm overall really digging the lispyness hiding within Lean's mixfix notation
on the topic of #Agda, I tried it a few winter holidays ago, reading Philip Wadler's PLFA, which is wonderful from the 1/3 I finished. it was a surreal experience compiling a book that proved the statements therein for 6 hours.
at some point after winter break, I switched distros, and never got around to recompiling the book, and so I never finished (I know I can just read the compiled version online, but I felt like reading the text from its literate agda files directly is a core part of the experience). I'll finish it one day, but I wonder if a #Chez backend would significantly reduce those compile times.
Hi, I'm Patrik Jansson, professor in the FP group at Chalmers. I just moved here from types.pl following some of my friends and colleagues.
Here is the text from my Profile:
Computer scientist, #Haskell hacker, catalyst of research ideas, likes to connect the big picture with formal details, software & language technology advocate.
Have worked on Domain-Specific Languages of Mathematics, #Agda, Climate Impact Research, Parametricity for Dependent Types, Testing, Parsing, polytypic programming, ...
More about me and my work can be found on my homepage: patrikja.owlstown.net/
@mousebot but here, I'll give it a shot based on vibes
Plato: #Agda (the Idea of the Good, proto-Maoist non-conformists)
Aristotle: #C (arch reactionary)
Duns Scotus: #ASM (simple brittle concepts but with plenty of haecceity)
Spinoza: #CommonLisp (OG that everyone thinks is fresh bcs its dynamic)
Descartes: #MLIR (ghost in the machine)
Kant: #CPP (critique of Pure C)
Hegel: #Genera (the absolute Idea as self-reflective system)
Nietzsche: #Scratch (the primacy of appearances)
Marx/Lenin: #ML (self-explanatory)
Freud: #GDB (not phil, but rather the original debugger for all the problems of phil)
Heidegger: #forth (the anti-technology technologist's lang of choice)
Wittgenstein: #Prolog (all there is are the facts)
Stalin: #Haskell (forces you to do things "correctly" even when its neither the best option for the situation nor the most performant; the extreme ML)
Lacan: #rr (meta-debugging, non-linear retroactive causality of the signifier, on top of gdb)
Deleuze: #MaxMSP (thinks programming should be art, thinks art is about infinite flows, elaboration of Nietzsche)
Federici: #SpritelyGoblins (super witchey)
Derrida: #AWK (theres nothing outside the text)
Malabou: #Python (everything is neurobiological including language itself)
Badiou: #Scheme (the generic is the Idea of the Good)
Butler: #Rust (the new generation of Kantians doing things right, performatively)
@quails@mousebot thinking about it more, Plato and Agda is definitely a bad match, because they are mostly constructivists, which is almost the polar opposite of Platonism. Perhaps #Agda is Cavailles, Plato is also scheme (Plato's Republic is a book by Badiou, fwiw)