3 ms·

> 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 oc

> 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. (I am one of the authors of Flix).

the-smug-one 6y ago
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?
- jorkadeen 6y ago
  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. (I am one of the authors of Flix)
  - the-smug-one 6y ago
    > 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 :-).
    - jorkadeen 6y ago
      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 :)
volta87 6y ago
Would be cool to be able to parametrize namespaces.
esarbe 6y ago
What's your take on Scala 3 (Dotty's) DOT calculus? edit: I'm asking because, from what I understand, the DOT calculus puts the Scala type system on sound foundations.
- jorkadeen 6y ago
  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.

the-smug-one 6y ago

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?

jorkadeen 6y ago
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. (I am one of the authors of Flix)
- the-smug-one 6y ago
  > 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 :-).
  - jorkadeen 6y ago
    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 :)

volta87 6y ago

Would be cool to be able to parametrize namespaces.

esarbe 6y ago

What's your take on Scala 3 (Dotty's) DOT calculus? edit: I'm asking because, from what I understand, the DOT calculus puts the Scala type system on sound foundations.

jorkadeen 6y ago
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.