I'm curious about the emphasis on fixpoints and lattices. These are two quite simple concepts often overlooked in CS and emphasized even less in programming languages. Lattices are natural to CS in that any time you have an order or even any binary relation, that imposes some structure on your values, and knowing the/solving for unique fixpoints (considering also continuity conditions) can be powerful, for instance the most general type of an expression, the "final" result of a recursive definition, infinite streams, final states of an imperative program and so on.
Seems to me that Flix would further blur the line between logic and functional programming (using what looks like some Prolog-esque search and datalog integration), amazing!
It's great to see structural typing in the form of polymorphic extensible records. But I am a bit disappointed they didn't go further, I would have at least liked to see extensible variants. The tuple-based syntax, also makes it rather noisy to use anonymous records as arguments (e.g. for named parameters).
If I was designing a new modern language, I would make the default types structural records and variants and use a single "new type" form for creating nominal types, when necessary. Compositional datatypes are much easier to achieve with structural records/variants (e.g. define a new enum set based on another). It is also trivial to make a structural type nominal, but not to go the other way. But having structural records as something special alongside nominal ADTs (like Flix, Elm and Purescript), does not exploit the duality and does not give a modern rethink that IMHO is needed.
By "compositional datatypes", I mean being able to define datatypes and functions on them in a modular fashion. I gave a very simple example with enums. For a real world use case, imagine a compiler pipeline, where we have an AST that we are desugaring over multiple steps. Ideally we want a succession of ASTs that remove the form being eliminated, so the AST type can guarantee it's eliminated. This is very easy with structural variants, there's no need to actually define and name each separate AST, which differs only slightly.
Or imagine we are typing a SQL join that is a merge of two existing record types. Such "compositional data types" can be achieved with elaborate encodings and type-level computations in a language like Haskell (see e.g. Data types `a la carte), but it's difficult and somewhat ugly. There is an opportunity here for improvement.
You can do this with the tagless-final encoding, which has a similar flavor to Data types à la carte's concept of open data types. As an example, define
class ExpSYM a where
add :: a Int → a Int → a Int
lit :: Int → a Int
class MulSYM a where
mul :: a Int → a Int → a Int
Now suppose we extend with booleans and so on. We can freely combine addition and multiplication. As we add new data variants, old code need not be recompiled. We get the openness of OOP's class extensions with the flexibility of ADTs.
ex1 :: (ExpSYM a, MulSYM a) => a Int
ex1 = add (lit 3) (mul (lit 4) (lit 5))
Not enough space here but you can also pattern match over final terms and interpret them in different ways (e.g. CBN vs CBV interpreters).
Then as you go through your compiler pass you can see through the types that "capabilities" get reduced more and more until you reach some base language (sounds like free monads doesn't it?).
Tangentially if I were to design an FP language I would use tagless final for everything, and deforest as much as I can (if possible) to reduce overhead. How this affects other aspects (e.g. automatically translating pattern matching) I have not looked into, but it's interesting nonetheless.
Yes, but like any encoding, it has its problems. One potential issue is that you will need to formulate your transformations as strict catamorphisms (folds), e.g. you cannot match two levels deep. This has reasoning advantages, but makes it harder for the average user. Type classes can also have issues with ambiguities, if many type variables are involved. Lastly, you also cannot match all remaining terms, like these examples:
getDates
:: Exp
-> Set Date
getDates = cata alg where
alg :: ExpF (Set Date) -> Set Date
alg (EDate i) = S.singleton i
alg e = fold e
substitute
:: Map VarId (ExpF Exp)
-> Exp
-> Exp
substitute env = cata alg where
alg :: ExpF Exp -> Exp
alg (EVar i)
| Just e <-M.lookup i env = Fix e
alg e = Fix e
Ah ha, but you see, you can perform transformations on tagless-final terms that are not strict catamorphisms. Oleg demonstrates this in (page 14)[0] with examples of reassociating binary expressions and double negation, so matching two levels deep is possible.
As for matching remaining terms, I don't know the answer to that, would be interesting to investigate.
Yeah, having many typeclasses involved could be problematic. What sort of issues are you thinking of? One possibility is that so many constraints are involved no concrete type can instantiate a final term.
> Ah ha, but you see, you can perform transformations on tagless-final terms that are not strict catamorphisms ... so matching two levels deep is possible.
No this is not correct. Oleg provides a solution to double negation by creating a catamorphism that folds to a function. It's still a catamorphism. And folding to a function is not something the average Java programmer is likely to understand easily.
Right, so it's not that it's not possible but rather it's somewhat awkward to express non-compositional folds in the final approach. I'm not currently aware of a mechanical way to do the translation.
Yes, I'm claiming the restriction will be too much for many people, assuming we are trying to create a new language here. However, expressing a solution as a catamorphism is a good thing to do and helps reasoning. It's a form of structured programming (recursion is the "goto" of functional programming!).
This seems to just about single-handly take my least favorite syntax feature from each of of the languages it cribs from... FS path based import, overly verbose types with too much &{}% noise, "let" noise, oh and it runs on JVM.
Edit: I'm not quite as negative as I sound, but given the headline (or the CTA on the homepage for that matter), I am much less than whelmed. This seems fine I guess, but just another "check all the boxes" language that doesn't really bring much of anything obvious new to the table.
> This seems fine I guess, but just another "check all the boxes" language that doesn't really bring much of anything obvious new to the table.
Flix aims to occupy a unique point in the design space. It combines features from programming languages like Go, Haskell, OCaml, and Scala in a way that no other language does. It has:
- a sound type system (like Haskell and OCaml)
- a complete local type inference algorithm (like Haskell and OCaml)
- eager evaluation (like OCaml and Scala)
- CSP style concurrency (like Go)
- type classes (like Haskell)
- full tail call elimination (like OCaml and Haskell)
If you look at the "Innovations" page you will find that Flix has (at least) two features found in no other programming language: a polymorphic type and effect system and first-class Datalog constraints.
Racket has delimited continuations (from which you can build effects w/o the types) and Datalog as a #lang. Sure, not a lot of types unless you use Typed Racket, that's true. I also don't see why you couldn't swap out Datalog with another constraint system, like that described in Monadic Constraints (Wadler, Stuckey, Sch-something).
I think the effect system is cool. How does Flix differ from Eff or Unison in this matter?
The Datalog implementation in Racket is neat, but does not support stratified negation nor are the Datalog constraint first-class. Both features make it significantly more practical to work with Datalog. Also, the Flix type system ensures - at compile-time - that all first-class Datalog values constructed at run-time are stratified.
The effect system in Flix is focused on a single effect: purity. It is very fine-grained (compared to e.g. systems based on rows) and it supports effect inference and effect polymorphism. Eff and Unison have richer effect systems - based on algebraic effects - which allow re-interpretation of effects. However these effects system struggle more with effect inference. For example, I believe that in Eff you only have a restricted form of effect polymorphism / the use of higher-order functions is more limited.
> Also, the Flix type system ensures - at compile-time - that all first-class Datalog values constructed at run-time are stratified.
That does sound powerful! To be honest I have no idea what the implications of that are - but I guess that's why it's research!
Re: effect system.
The reason that I think algebraic effects are so cool is that they allow for trackable, side-effectful, and powerful abstractions.
To me it sounds like Flix's Pure/Impure effects offer a fine-grained form of taint tracking. Why do you think I should be excited about this? For example, why not Haskell's monad solution?
I hope I don't come off as confrontational, I'm genuinely interested :-).
I think you would want both: algebraic effects and very fine-grained effect reasoning. For example, in all most all languages it is vital that functions such as "equal" and "hash" are pure. It is an open problem how to combine our fine-grained Boolean unification-based effect system with other algebraic effect systems (e.g. row polymorphic ones). I hope the future will tell :)
My understanding is that there are 15+ papers that formalize and prove soundness of various aspects of the DOT type system, but that the "full" type system implemented in Dotty today is still unsound. Hopefully this situation will improve in the future.
> This seems fine I guess, but just another "check all the boxes" language that doesn't really bring much of anything obvious new to the table.
Full disclosure: I have contributed a small amount of code to the standard library of Flix.
Personally I find the inclusion of Datalog as a first-class citizen in an otherwise functional language to be a pretty powerful feature that I personally haven't really seen done before.
> Personally I find the inclusion of Datalog as a first-class citizen in an otherwise functional language to be a pretty powerful feature that I personally haven't really seen done before.
It's neat, but IIUC, it needing to be a language feature (versus being included as a library) emerges from the lack of macro support. That's one of my issues with non-macro languages, I have to wait for the language owners to add this stuff.
In Flix, Datalog constraints are first-class values. This is strictly more powerful than a macro system. For example, the Datalog programs that are constructed can depend on input values to the program. This is not the case for macros which are expanded compile-time. (Unless you have some kind of reflection in mind...)
EDIT: I hope to explore a macro system for Flix in the future. So we are definitely on the same side of the issue; just wanted to point out that the current system is more powerful.
This actually looks like a language I would like to use. Datalog like constraints were surprising. The current state of JVM interoperability makes it clear though this is a research project.
Could this be ported to other "hosting" languages/VMs? In any case, I think interoperability with foreign code needs a different solution and it has to have a way to fully deal with OOP constructs.
Same for me, Flix looks like a language I would use professionally. It has that powerful OCaml/F# vibe.
Built-in Datalog is indeed a surprising feature. Strongly reminded me that we may come to a universal data model someday just like we rely on universal computational model (Turing / von Neumann) nowadays. Under that model, we would not make distinctions between various sources of data and we would be able to efficiently query them in every structural dimension they offer.
Pure speculation on my part (since I couldn't find any details either): their "Closed world assumption" and "No reflection" principles [1] could mean the compiler can output radically different bytecode, e.g., eliminating the tail call by eliminating the "call" altogether. That said, I might be wrong given that the FAQ [2] notes that tail call elimination "has some run-time performance cost"; maybe they're baking in a trampoline.
At the moment it uses a technique called "Impure Functional Objects" - which are a form of reusable stack frames. In the future we may switch to trampolines and eventually if Project Loom succeeds we will try to use whatever infrastructure they come up with.
> Can we just stop building new programming languages?
We build new programming languages and we do research on programming languages because we want to offer developers better tools to write programs. We want tools that make it simpler, safer, and faster to write correct programs. We want tools that increase productivity and that aid in program maintenance.
The situation is not unlike why we would want better airplanes, better houses, or better surgical instruments.
Why not NaN for floating point division and INT_MAX for integer division?
When you write code that may divide by zero you need to check the result afterwards (and in truly defensive programming that is every time you divide numbers). 0 is not a great choice because it doesn't necessarily mean you divided by zero - in floating point, dividing by a sufficiently large number or when working with the status register set to flush denormals to zero then normal division can result in 0. For integer division, any fraction will result in 0.
- introduce a non-zero number type, define division as Number/NonZeroNumber -> Number, and provide a simple, non-verbose way to convert a Number into NonZeroNumber (with default value in case of zero, and/or direct assignment after a non-zero-check)
- optionally introduce an unsafe division operator that takes two Numbers and returns Option[Number]
@jorkadeen since you're here: the landing page's two-column layout doesn't work great on mobile, you get two columns that are like 2-words wide:
Recent | Bread-
News | and Butter
| Functional
2020-11-20 | Programming
We are on |
Twitter! Find | Flix supports
us at | basic building
@flixlang. | blocks of typed
| functional programs
(Android, recent Firefox)
it'd probably be good to switch the divs to `class="col-xs-12 col-md-6"` or equivalent
"Alternatively, Flix can be thought of as a functional programming language with a very powerful embedded query language. A Flix programmer can use first-class Datalog constraints to simply, elegantly, and efficiently solve fixpoint computations inside functional code. It should be noted that Datalog is strictly more expressive than relational algebra (~= simple SQL)."
So IIUC, the effect system [2] means impurity is contagious. This seems reasonable to me, though I wonder what that means in practice. `Console.printLine` is impure [3], and presumably any debug logging would be too; the contagion might spread pretty far. I wonder if this is why seemingly pure functions like `Array.find` are flagged as impure [4].
> Principle of least surprise: ... and when there is no immediately obvious default, we should not have a default at all, but force the programmer to be explicit about his or her intention.
I like that they called this part out. I'd wager most code really doesn't have sane defaults, just the defaults that made sense to the developer at the time.
> Local type inference
I find that in languages with type signatures (without inference), folks lean on the type to convey information, and in dynamic languages like Clojure, folks lean on good naming. Based on my not-much experience with type inference, the code ends up with neither. Sure the compiler can figure out what it is, but the humans not so much.
> Uniform function call syntax: ... the function call length(xs) can also be written as xs.length()
I wonder what their motivation was for this; my guess is to appeal to both FP and OO devs. IMO, having multiple ways of writing the same thing is likely to lead to unnecessary style wars.
> Private by default: ... declarations are hidden by default (i.e. private) and cannot be accessed from outside of their namespace
I like this a lot, though I foresee running into issues with unit testing, and thereby arguments over at what level things should be tested.
> Bugs are not recoverable errors: ... For recoverable errors, we should enforce that they are checked and handled. For program bugs, we should terminate execution as quickly as possible
This seems reasonable to me, but I'm curious what counts as a "program bug", or how to know that some error is recoverable.
> No null value
Meh. I've think Option is just null with extra steps. NPEs arise because of method invocation, e.g., `x.foo()` while `x` is null. In FP languages like Clojure, NPEs don't really happen since `x` is just a value being passed to a function. With nil-punning and reasonable behavior of core functions (e.g., `(get m k)` yields nil when `m` is nil), an unexpected nil is really a type error.
> No dead or unreachable code / No unused variables
Perhaps it's from my REPL-driven, exploratory style of development, but I think having to constantly comment out code I'm ambivalent about just to get it to compile would be a bit annoying. I'd think something like this should be a compile option, but I think that runs afoul of their "One Language"/"no flags" principle.
> No variadic (varargs) functions
Having worked with enough Clojure, and seen enough bugs when using `apply` on vararg fns, I think this is a good choice. IIUC, their approach would replace, e.g., `(+ x y z ...)` with `(sum [x y z ...])`.
> No binary or octal literals: ... It is our understanding that these features are rarely used in practice.
Until you need to do some bit-twiddling; maybe they still have hex. I wonder what they considered the downside of including it.
> Meh. I've think Option is just null with extra steps.
Yeah, but those extra steps are worth it. I've written a fair bit of typescript and javascript, and I feel like I need to be always careful about nullable values in javascript. Like, I agree that Option is null with extra steps - but those extra steps make it harder for bugs to creep into my code.
In JS its all too easy to accidentally write getNullableVal().doStuff(). Or doStuffWith(nullableVal) and inside the function accidentally forget that the value can be null. In typescript the compiler forces me to consider the nullable case for nullable values, and as a result my code ends up better. And when I pass a nullable value into a method, its clear from the type signature whats going on. I still make bad assumptions sometimes and unwrap when I shouldn't, but when crashes happen they happen closer to the bug in the code.
My favorite syntax for all this is Swift, which understands nullable types at a language level. (Rather than at the type level in rust / haskell). It means the language can coerce X -> Just(X), so making function arguments nullable doesn't break callers. And let myVal: SomeType? / myVal!.foo() syntax seems strictly better than rust's let myVal: Option<SomeType> / myVal.unwrap().foo().
> Based on my not-much experience with type inference, the code ends up with neither. Sure the compiler can figure out what it is, but the humans not so much.
A decent IDE should make the type information available when you need it.
> This seems reasonable to me, but I'm curious what counts as a "program bug", or how to know that some error is recoverable.
I would assume recoverable errors would be explicitly represented in an Either-like style, and if you don't have a better way to handle them you can explicitly turn them into a program bug (exception/panic) by some unwrap()-like operation.
> an unexpected nil is really a type error.
Right, which is why you want "nullable x" to be distinct from "x" in the type system. The problem isn't the NPE per se, it's silently allowing the program to continue in an invalid state until the error happens far away from the problem that caused it, and that's just as much of a problem in Clojure.
And so either you create a special ad-hoc thing in your type system with a bunch of syntax and special cases in the language standard that misbehave when your users do something you didn't anticipate, or you can write a normal datatype to represent "nullable x" and everything will just work, and then maybe put some lightweight syntax sugar on top if you really want to.
> A decent IDE should make the type information available when you need it.
A decent programming language shouldn't need an IDE to understand the code. What happens when you post a snippet online ? Or when you look at a diff in github ?
Why? Why make the common, important case worse for the sake of the uncommon case?
In any language you have to make a tradeoff between concision and explicitness. With type inference you could write code whose text is just as explicit as you'd do in an untyped language, and use the types solely to provide more detail. Or you could put no more detail than in an untyped language, but move some of that detail into types and make your code more concise. Most people find a point somewhere in the middle, and end up with code that's both more concise and more explicit (when you look at the types); of course that means the code is more "magic" if you're looking solely at the text.
Merge requests/Pull requests are definitely an integral part of development, I don't think you can say it's an uncommon case. Same goes for sharing snippets with colleagues to explain/understand ehat is happening. Even Go has shown that there is value in not putting a lot of context in every single word of your language: it makes it longer to write, but easier to read whrn you have no prior experience of said piece of code.
There is definitely a balance to be found, but I believe most languages today (and, unfortunately, programmers) rely too much on an IDE even though there's a large enough part of our work happening outside of it.
> Merge requests/Pull requests are definitely an integral part of development, I don't think you can say it's an uncommon case.
Reviewing PRs is important, but you'd normally do it from a development machine with your normal tooling available; I don't think it's too big an imposition to say you should do it with an IDE, or else accept that you will have slightly less context available. (In some ways it's good to review that way, as it means you evaluate whether the code is still clear even with less information available).
> Same goes for sharing snippets with colleagues to explain/understand ehat is happening.
I hardly ever see that happen; it's usually much better to create a branch or worksheet.
> There is definitely a balance to be found, but I believe most languages today (and, unfortunately, programmers) rely too much on an IDE even though there's a large enough part of our work happening outside of it.
IMO it's just the opposite; there's a lot of good things we can do with the GUI tools that we realistically ~always have available. Programmers are rightly sceptical of "visual programming" tools that break VCS history, but a language that has an understandable textual representation enhanced by the GUI gets you the best of both worlds.
You've written a lot, and I can't respond to everything. I'd just like to point out that the Array type is backed by proper JVM arrays. Operations on those are inherently impure. For a better representation of the effect system on a collection I'd suggest looking at the List type instead.
Source: i worked a bit with the language during Spring.
It just struck me as odd for reads like `find` (which itself requires a pure fn arg). Is that because given the same reference, the function could yield different outputs? Or because it could be mutated concurrently? Would that imply every function that takes a mutable data structure will be impure?
Edit: I just noticed that `List.toArray` -- which just returns a new array, so no concern over references or mutation -- is also marked as impure. This seemed wrong to me, but then I noticed that even `Array.new()` is marked impure. To my mind, a function that allocates a new mutable collection is itself not inherently impure.
> Would that imply every function that takes a mutable data structure will be impure?
That always has to be true, no? Reading from a mutable datastructure is impure in the same way that reading from standard input is.
> Edit: I just noticed that `List.toArray` -- which just returns a new array, so no concern over references or mutation -- is also marked as impure. This seemed wrong to me, but then I noticed that even `Array.new()` is marked impure. To my mind, a function that allocates a new mutable collection is itself not inherently impure.
Two different arrays with the same members are not generally equivalent. E.g. (x.toArray, x.toArray) is semantically something very different from {val y = x.toArray; (y, y)}.
> That always has to be true, no? Reading from a mutable datastructure is impure in the same way that reading from standard input is.
If the function internally reads from stdin, I'd agree. But if a fn takes an input stream as an arg, and if given input streams that yield the same bytes the fn always yields the same result, then why consider it an impure fn? The input stream is just a fancy data structure for bytes.
> Two different arrays with the same members are not generally equivalent.
Derp, of course! And though I guess it would be possible to have the `Mut*` collections use value equality instead of reference equality, that'd probably conflict with the performance goals of the mutable variant.
> But if a fn takes an input stream as an arg, and if given input streams that yield the same bytes the fn always yields the same result, then why consider it an impure fn? The input stream is just a fancy data structure for bytes.
Hmm. It's impossible to create a value that's equivalent to reading from the input stream, because reading from the input stream has operational effects. But that logic doesn't apply to an array if your access to the array is unobservable. (One could argue that reading from an array creates temporal relationships, but I don't think that really holds up). So I think you're right, and a function that accepts a mutable datastructure can still be pure (in a vacuous sense really, since a mutable datastructure can't ever be equivalent to a value - it's not even equivalent to itself at a different time), though given that that purity can't ever be useful to you I don't think it's particularly important.
> And though I guess it would be possible to have the `Mut*` collections use value equality instead of reference equality, that'd probably conflict with the performance goals of the mutable variant.
It's not about the implementation of .equals(), it's about semantic equivalence. Two different arrays with the same members behave quite differently than two references to the same array (as the program continues and other code mutates them), regardless of whether they compared equal at the start.
We are still figuring out the details about array impurity. But in a nutshell if something is pure it should support substitution. For example:
let x = 123;
let y = (x, x)
If you substitute x into the pair you get the same result. So far, so good.
Now consider:
let x = [1, 2, 3];
x[0] = 5;
let y = x[0]
If you substitute x into the body of y you get a different result! The meaning of x[0] changed underneath you. We are very conservative and say that anything which touches an array is impure. Is this the best solution? no- but it is a reasonable/sound start.
> But in a nutshell if something is pure it should support substitution.
Neat, hadn't thought about it like that before.
> If you substitute x into the body of y you get a different result!
Heh, I guess that depends on "which" x. I recognize Flix doesn't allow shadowing as a defensive choice, but with respect to substitution, wouldn't this be equivalent to something like:
let x = [1, 2, 3]
let x = insert(0, 5, x) # treating it like Map [1]
let y = get(0, x)
IOW, it's not clear to me why the `x[0] = 5` step would be skipped when considering substitution. Hmm, per the substitution principle, is `x[0] = 5` pure?
> We are very conservative and say that anything which touches an array is impure.
Understandable given how difficult it is to reason about mutable things.
----
[1] Given the uniform function call syntax, I found it odd that the map is the last arg in the function. I originally assumed it would be m.insert(k, v) === insert(m, k, v)
> Meh. I've think Option is just null with extra steps.
Better to concentrate on the plain "A" in "Option[A]" I think. WHen you don't have nulls, Option is what allows you to have plain types that don't use Option, that can't be "missing", which is enforced by the type system, and so doesn't need any "steps" at all to handle them as regards presence/absence of value.
> Meh. I've think Option is just null with extra steps.
It is when you don't use it right. Although, you have the benefit of being explicit about it. Still, you're supposed to make your Option/Maybe type a monad and functor, so you can easily chain Option/Maybe-returning functions and transformations while hiding all the boilerplate null checks.
For example: Given the type List[Int] the cons cells of each list contain a primitive integer and a pointer to the next cons cell. (In Java, you would instead have List[Integer] where each element of the list is a boxed/wrapped Integer object). I hope that answers your question?
Unboxed integers is no big feat. Many implementations of garbage collected languages have unboxed small scalars (OCaml and Guile come to mind).
What about compound types?
Adding to that: effect inference and polymorphism, unboxed primitives, full tail call elimination, extensible records, first-class Datalog constraints, CSP style concurrency, a multitude of different design choices.
While it may be faster, the "by definition" part hasn't been true for years. The JVM can do some amazing stuff at runtime to outpace statically executed code.
Regardless, their principles [1] make the trade-offs clear:
I’m not an expert but my understanding is that modern JIT can be faster than ahead of time compilation because the JIT has runtime information, so you get profile guided optimization for free.
Warm up takes a while but then it can be very fast. For long running servers this works quite well.
Has anyone tried runnig those benchmarks with AOT Java? Microbenchmarks like these tell absolutely nothing about general performance because they are short-lived. JVM is a beautiful piece of engineering and I believe you guys chose well this platform to host it, always hoped for a ML-inspired language running on the JVM and this looks like it.
Seems to me that Flix would further blur the line between logic and functional programming (using what looks like some Prolog-esque search and datalog integration), amazing!