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:
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!
#NowPlaying Grant Green - Alive! (Blue Note, 1970). Recorded live at the Cliché Lounge, Newark, NJ on 8/15/1970. Jazz-funk (or is it funky jazz?) was my gateway from hip-hop to jazz. The closing track Down Here On The Ground is instantly recognizable from the sample on A Tribe Called Quest - Vibes and Stuff. Anything with Idris Muhammad on drums is worth listening to. #jazz#funk#hiphop#GrantGreen@vinylrecords
@BEK97@vinylrecords Maiden Voyage is a bonus track? Insane. It's one of the best things I've heard in my life. #Idris is a monster on this record--kicks the band into another realm.
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.
Meaning of the linear arrow: f :: s ⊸ t guarantees that if (f u) is consumed exactly once,then the argument u is consumed exactly once(Consume exactly once).to consume exactly once • (like Int or Ptr) - just evaluate it.• unction value -apply it to one argument, consume its resultexactly once.• pair - pattern-match on it, consume each component exactlyonce.• adt, pattern-match on it,, all its linear components a linear arrow specifies how f uses its argument. It does not restrict
arguments to which function can be applied.a linear f cannot assume that itis given unique pointer to its argument. For example, if f :: s ⊸ t, then this is fine:g :: s → tg x = f xThe type of g makes no particular guarantees about the way in which it uses x; in particular, g canpass that argument to f.result of (unsafeFreeze ma) is a new immutable array, but toavoid an unnecessary copy, it is actually ma. The intention is, of course, that that unsafeFreezeshould be the last use of the mutable array; but nothing stops us continuing to mutate it further,with quite undefined semantics. The “unsafe” in the function name is a ghc convention meaning“ programmer has a proof obligation here that the compiler cannot check”.other unsatisfactory thing about the monadic approach to array construction is that it isoverly sequential. Suppose you had a pair of mutable arrays, with some updates to perform to each;these updates could be done in parallel, but the ST monad would serialise them
• Operations on files remain monadic, unlike the case with mutable arrays. I/O operations
affect world, hence must be sequenced. It is not enough to sequence operations on
files individually, as it was for arrays.
• generalise the IO monadst it expresses whether or not returned value is linear.
extra multiplicity type parameter p to the monad IOL, where p can be 1 or ω,
indicating a linear or unrestricted result, respectively. Now openFile returns IOL 1 File, the “1”
indicating that the returned File must be used linearly.
• As before, operations on linear values must consume their input and return a new one; here
readLine consumes the File and produces a new one.
• Unlike the File, the ByteString returned by readLine is unrestricted, and the type of readLine
indicates this.
Uniqueness (or ownership) types ensure that an argument of a function is not used elsewhere in an expression’s context even if the callee can work with the argument as it pleases. Linear types and uniqueness types have a ‘weak duality:’ ‘Seen as a system of constraints, uniqueness typing is a non-aliasing analysis, while linear typing provides a cardinality analysis.’1
API for pure mutable arrays, the original Linear #Haskell paper [2] (Arxiv version) featured the function:newMArray :: Int -> (MArray a %1 -> Ur b) %1 -> Ur b
Taking a linear function as an argument, newMArray can make sure that the MArray is, in fact, not aliased. This is because linear types only restrict how a function can use an argument, it can’t restrict how the context uses an argument or a returned value. Contrast with uniqueness types (aka ownership types) in languages like Rust or Clean, which can demand that a value not be aliased. So, whenever we use linear types, in Haskell, to implement an API with a uniqueness requirement, we end up with such a newX function that takes a linear-function argument With newMArray and newMArrayBeside we have two functions to create new arrays. This isn’t satisfactory, but it gets worse. If I have another type with uniqueness constraints, say a ring buffer, then I’ll eventually need the ability to allow a ring buffer to piggyback on an array’s scope, and an array to piggyback on a ring buffer’s scope. with n types that can only be used linearly, I’ll need n^ 2 new functions. This is simply not sustainable. 3
of the many problems with Monads, one of them is that they are not composable, and Monad transformers are just a hack, you still have a stack of monads and how they interact when control flow gets involved can be hard to predict. Compare this with uniqueness typing (and syntax sugars for in/out arguments) and it's trivial to have multiple states used by the same function 4
Linearity via ST monads{ phantom type parameter s} -( region) that is instantiated once at start ofcomputation by a runST function of type:runST :: ∀a. (∀s. ST s a) → aresources that are allocated during computation,eg mutable cell references,cannot escape the dynamic scope of the call to runST because they are themselves tagged with thesame phantom type parameter.Region-types. With region-types such as ST, we cannot express typestates, but this is sufficientto offer a safe api for freezing array or ensuring that files are eventually closed. This simplicity(one only needs rank-2 polymorphism) comes at a cost: we’ve already mentionned in Sec. 2.2 that itforces operations to be more sequentialised than need be, but more importantly, it does not supportprima facie the interaction of nested regions.Kiselyov and Shan [2008] show that it is possible to promote resources in parent regions toresources in a subregion. But this is an explicit and monadic operation, forcing an unnatural imperative style of programming where order of evaluation is explicit. The HaskellR project [Boespfluget al. 2014] uses monadic regions in the style of Kiselyov and Shan to safely synchronise valuesshared between two different garbage collectors for two different languages. Boespflug et al. reportthat custom monads make writing code at an interactive prompt difficult, compromises code reuse,forces otherwise pure functions to be written monadically and rules out useful syntactic facilitieslike view patterns.In contrast, with linear types, values in two regions hence can safely be mixed: elements can bemoved from one data structure (or heap) to another, linearly, with responsibility for deallocationtransferred along.t everything which must be single-threaded – and that we would track with linearity – becomepart of the state of the monad. For instance, coming back to the sockets of Sec. 5.2, the type of bindwould be as follows:bind :: (sock :: Var) → SocketAddress → ST IO () [sock ::: Socket Unbound :7→ Socket Bound]Where sock is a reference into the monads’s state, and Socket Unbound is the type of sock beforebind, and Socket Bound, the type of sock after bind.Idris uses its dependent types to associate a state to the value of its first argument. Dependenttypes are put to even greater use for error management where the state of the socket depends onwhether bind succeeded or not:-- In Idris, bind uses a type-level function (or) to handle errorsbind :: (sock :: Var) → SocketAddress →ST IO (Either () ()) [sock ::: Socket Unbound :7→ (Socket Bound ‘or‘ Socket Unbound)]-- In Linear Haskell, by contrast, the typestate is part of the return typebind :: Socket Unbound ⊸ SocketAddress → Either (Socket Bound) (Socket Unbound)The support for dependent types in #ghc is not as comprehensive as #Idris . But it is conceivable toimplement such an indexed monad transformer in #Haskell. an existing lazy language, such as Haskell, can be extended withlinear types, without compromising the language, in the sense that:• existing programs are valid in the extended language without modification,• such programs retain the same operational semantics, and in particular• the performance of existing programs is not affected,• yet existing library functions can be reused to serve the objectives of resource-sensitiveprograms with simple changes to their types, and no code duplication.https://arxiv.org/pdf/1710.09756.pdf
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
Been relatively offline as of late. On the upside, I've landed a decent contract for the next few months leading the development of a SAAS startup, which means I'm experiencing a bit of stability for the first time in many moons. On the downside, I'm under NDA and can't share any of the stuff I'm working on, and have had no free time to hack on Scheme.
As I'm doing CG work again, I'm considering diving into #SICM. I've loved the first two chapters of LiSP, but as its not really tied to what I'm working on atm, its hard to find time to dedicate to it. I'm a bit scared of SICM, as even a friend who studied physics (and has read SICP) said he found it to properly difficult. But I think if I go in assuming the book will take a year at minimum to complete, and allow myself to take my time without trying to schedule according to abstract expectations, it could be just the right time to brave the beast.
@ArneBab at that time (2020) I had just finished the #Idris book and was totally sold on static types, and was planning to follow it up with Software Foundations. Then a friend suggested I check out the TLS, which appeared as something like a work of art, and got me buzzing like nothing else. So then I started making my way through SICP, and was learning typed racket at the same time. But about a year after installing Guix, I decided to invest my time in #Guile — where I found myself lost whenever I'd try to use it outside of Guix — and my interest in types has gradually faded as I've gone further and further down the rabbit hole.
I still plan to read SF eventually, but my interests have changed dramatically the more and more I've become captivated by #lisp, and I feel content with my decisions.
@pkw everytime I try to get into Haskell I wind up going down the rabbit hole of dependently typed languages. After reading the Idris book a few years ago I got a glimpse of programming with typed holes, and while wingman does a pretty good job in Haskell, its missing the richness that comes from the type-value dependence, which allows you to use synthesis in a more "dependable" way (I know I've found myself stuck trying to get a wingman to synthesize a hole that I thought it should understand, to no avail, where with #idris you can narrow down the search space pretty surgically)
@daviwil@PaniczGodek but in all fairness, I think interest in Scheme has been growing due to #Unison's adoption of Chez for their primary backend and 470x performance increase they saw as an immediate result.
The average person seems to think that scheme is a slow toy language for learning how to implement programming languages, which is just incredibly wrong as demonstrated by projects like #idris, #guix, #goblins and countless others. #scheme is C among functional languages.
To be fair, I think Haskell will continue to fill the niche it filled ~10 years ago, around the time it started to get mainstream hype. Small teams of skilled devs delivering robust products that would normally require much larger teams to maintain will continue to prevail. Purely functional lazy programming was never bound for world domination in an economy which is antagnostic to curiosity, creativity and truths.
On the other hand, I have the feeling that we're going to see more and more Haskellers-turned-Rustaceans come to realize that #Rust does little to alleviate the primary barrier to Haskell's wider success -- fast and predictable turnaround time for projects developing cutting-edge technologies -- and will wind up going the same route as some major Haskell projects such as #Unison and #Idris have in recent years, which is to try #Chez Scheme, only to discover that it allows them to release blazing fast functional programs on a generic foundation where major breaking changes are practically non-existent, providing incredible flexibility while significantly reducing dependencies by dint of the ad-hoc tooling that falls out of the bottom of #scheme. Not to mention the joys that come from near-instant startup times, some of the fastest compile time you've ever encountered, fully-customizable interactive development and a surgical #debugger that rivals Haskell in scheer fun. Yesterdays naysayers will become tomorrow's enthusiastic bootstrappers. Or a at least a boy can dream.
That said, in all seriousness I don't think Scheme will ever reach the heights of Haskell's moderate commercial success. But I do think that projects built on Scheme, like Unison, will get a leg up and eventually surpass it, and interest in #lisp will only grow.
@nilmethod sbcl is generally faster than most schemes (but chez certainly gives it a run for its money), but #guile and #chez are incredibly fast in terms of start up and compile times. I read somewhere that chez bootstraps #idris in about 2 minutes, for example (I think #haskell took over 20 minutes when it was the implementation language).