-
-
+
+
+
-
-
-
+
diff --git a/src/App.css b/src/App.css
index ae387ec..cb25a79 100644
--- a/src/App.css
+++ b/src/App.css
@@ -1,96 +1,97 @@
body {
- font-family: 'Open Sans', sans-serif;
- overflow-y: scroll;
+ font-family: 'Open Sans', sans-serif;
+ overflow-y: scroll;
- background-color: #efefef;
+ background-color: #efefef;
}
h1 {
- font-size: 2rem;
- margin-bottom: 0.75rem;
- text-align: left;
+ font-size: 2rem;
+ margin-bottom: 0.75rem;
+ text-align: left;
}
h2 {
- font-size: 1.7rem;
- margin-bottom: 0.75rem;
- text-align: left;
+ font-size: 1.7rem;
+ margin-bottom: 0.75rem;
+ text-align: left;
}
h3 {
- font-size: 1.6rem;
- margin-bottom: 0.75rem;
- text-align: left;
+ font-size: 1.6rem;
+ margin-bottom: 0.75rem;
+ text-align: left;
}
p:last-child {
- margin-bottom: 0;
+ margin-bottom: 0;
}
.menu {
- margin-left: -15px;
- margin-right: -15px;
+ margin-left: -15px;
+ margin-right: -15px;
}
.page {
- background-color: white;
- min-height: 95vh;
+ background-color: white;
+ min-height: 95vh;
}
.motto {
- font-size: 1.35rem;
- color: #17a2b8;
+ font-size: 1.35rem;
+ color: #17a2b8;
}
.editor-output h5 {
- font-size: 1.1rem;
- color: gray;
- text-align: center;
- padding-bottom: 0.5rem;
- border-bottom: 1px solid #b7b7b7;
+ font-size: 1.1rem;
+ color: gray;
+ text-align: center;
+ padding-bottom: 0.5rem;
+ border-bottom: 1px solid #b7b7b7;
}
.editor-output pre {
- font-family: monospace;
+ font-family: monospace;
}
.inline-editor-frame {
- margin-top: 1em;
- margin-bottom: 1.5em;
+ margin-top: 1em;
+ margin-bottom: 1.5em;
}
.inline-editor-code {
- padding: 1em 1.5em;
- background-color: #f7f7f7;
+ padding: 1em 1.5em;
+ background-color: #f7f7f7;
}
.nav-item {
- cursor: pointer;
+ cursor: pointer;
}
.navbar-nav .nav-item .nav-link {
- color: rgba(255, 255, 255, .85)
+ color: rgba(255, 255, 255, 0.85);
}
.navbar-nav .nav-item .nav-link:hover {
- color: rgba(255, 255, 255, 1.00)
+ color: rgba(255, 255, 255, 1);
}
-.btn-group .btn, .btn-xs {
- padding: .1rem .5rem;
- font-size: .875rem;
- line-height: 1.5;
- border-radius: .2rem;
+.btn-group .btn,
+.btn-xs {
+ padding: 0.1rem 0.5rem;
+ font-size: 0.875rem;
+ line-height: 1.5;
+ border-radius: 0.2rem;
}
.card-title {
- font-size: 1.2rem;
+ font-size: 1.2rem;
}
.ace_hidden-cursors {
- opacity: 0
+ opacity: 0;
}
.w-33 {
- width: 33%;
+ width: 33%;
}
diff --git a/src/App.js b/src/App.js
index b7f9453..cf5496b 100644
--- a/src/App.js
+++ b/src/App.js
@@ -1,152 +1,168 @@
-import React, {Component} from 'react';
-import './App.css';
-
-import Home from "./page/Home";
-import GetStarted from "./page/GetStarted";
-import Documentation from "./page/Documentation";
-import Principles from "./page/Principles";
-import Contribute from "./page/Contribute";
-import Research from "./page/Research";
-import Faq from "./page/Faq";
-import Checklist from "./page/misc/Checklist";
-import {Container, Navbar, Nav, NavItem, NavLink, Row} from 'reactstrap';
-import {Route} from "react-router";
-import {Link} from "react-router-dom";
-
-import ReconnectingWebSocket from 'reconnecting-websocket';
-import About from "./page/About";
-import Blog from "./page/Blog";
-import Koans from "./page/Koans";
-import Internships from "./page/Internships";
-
-const SocketAddress = 'wss://evaluator.flix.dev/ws';
+import React, { Component } from 'react'
+import './App.css'
+
+import Home from './page/Home'
+import GetStarted from './page/GetStarted'
+import Documentation from './page/Documentation'
+import Principles from './page/Principles'
+import Contribute from './page/Contribute'
+import Research from './page/Research'
+import Faq from './page/Faq'
+import Checklist from './page/misc/Checklist'
+import { Container, Navbar, Nav, NavItem, NavLink, Row } from 'reactstrap'
+import { Route } from 'react-router'
+import { Link } from 'react-router-dom'
+
+import ReconnectingWebSocket from 'reconnecting-websocket'
+import About from './page/About'
+import Blog from './page/Blog'
+import Koans from './page/Koans'
+import Internships from './page/Internships'
+
+const SocketAddress = 'wss://evaluator.flix.dev/ws'
class App extends Component {
- constructor(props) {
- super(props);
-
- this.state = {
- connected: false
- };
-
- console.log("Connecting to: " + SocketAddress);
-
- let options = {
- connectionTimeout: 2500
- };
-
- this.websocket = new ReconnectingWebSocket(SocketAddress, [], options);
-
- this.websocket.addEventListener("open", event => {
- console.log("Connected to: " + SocketAddress);
- this.setState({connected: true});
- });
- this.websocket.addEventListener("close", event => {
- console.log("Disconnected from: " + SocketAddress);
- console.log(event);
- this.setState({connected: false});
- });
- this.websocket.addEventListener("error", event => {
- console.log("Disconnected from: " + SocketAddress);
- console.log(event);
- this.setState({connected: false});
- });
- }
+ constructor(props) {
+ super(props)
- runProgram = (src, callback) => {
- if (!this.state.connected) {
- console.log("Not connected yet");
- return;
- }
+ this.state = {
+ connected: false,
+ }
- this.websocket.onmessage = event => {
- console.log("Received reply from: " + SocketAddress);
- const data = JSON.parse(event.data);
+ console.log('Connecting to: ' + SocketAddress)
- console.log(data);
- callback(data);
- };
+ let options = {
+ connectionTimeout: 2500,
+ }
- let data = {
- src: src
- };
+ this.websocket = new ReconnectingWebSocket(SocketAddress, [], options)
+
+ this.websocket.addEventListener('open', event => {
+ console.log('Connected to: ' + SocketAddress)
+ this.setState({ connected: true })
+ })
+ this.websocket.addEventListener('close', event => {
+ console.log('Disconnected from: ' + SocketAddress)
+ console.log(event)
+ this.setState({ connected: false })
+ })
+ this.websocket.addEventListener('error', event => {
+ console.log('Disconnected from: ' + SocketAddress)
+ console.log(event)
+ this.setState({ connected: false })
+ })
+ }
+
+ runProgram = (src, callback) => {
+ if (!this.state.connected) {
+ console.log('Not connected yet')
+ return
+ }
- this.websocket.send(JSON.stringify(data));
- };
+ this.websocket.onmessage = event => {
+ console.log('Received reply from: ' + SocketAddress)
+ const data = JSON.parse(event.data)
- getHome() {
- return - Flix is a functional-, logic-, and imperative- programming language focusing on making it - simple to write safe, robust, and elegant programs. It tries to achieve this through a - combination of a strong static type system with type inference, an extensive collection of - compile-time checks, and by - avoiding many of the mistakes of programming languages past. Flix aims to have a principled - design that does not sacrifice safety nor elegance at the altar of expediency. Flix - is a language for programmers that care about programs. -
- -- Flix draws inspiration from many other excellent languages, including Elm, F#, OCaml, - Haskell, Rust, and Scala. Flix visually resembles Scala with an emphasis on conciseness and - the use of keywords. We believe that short keywords are a useful visual aid when scanning - through source code and trying to quickly understand its structure. The static type system - of Flix supports (local) type inference and is based on Hindley-Milner like those of OCaml - and Haskell. The concurrency model of Flix is based on channels and processes as known from - Go. Flix aspires to have understandable and detailed error-messages like those found in Elm. -
- -- The Flix language and compiler is open source and freely available under the permissive - Apache 2.0 license. -
- -- The much celebrated hello world program in Flix: -
- -+ Flix is a functional-, logic-, and imperative- programming language focusing on making it simple to write + safe, robust, and elegant programs. It tries to achieve this through a combination of a strong static type + system with type inference, an extensive collection of compile-time checks, and by avoiding many of the + mistakes of programming languages past. Flix aims to have a principled design that does not{' '} + sacrifice safety nor elegance at the altar of expediency.{' '} + Flix is a language for programmers that care about programs. +
+ ++ Flix draws inspiration from many other excellent languages, including Elm, F#, OCaml, Haskell, Rust, and + Scala. Flix visually resembles Scala with an emphasis on conciseness and the use of keywords. We believe + that short keywords are a useful visual aid when scanning through source code and trying to quickly + understand its structure. The static type system of Flix supports (local) type inference and is based on + Hindley-Milner like those of OCaml and Haskell. The concurrency model of Flix is based on channels and + processes as known from Go. Flix aspires to have understandable and detailed error-messages like those + found in Elm. +
+ ++ The Flix language and compiler is open source and freely available under the permissive Apache 2.0 + license. +
+ +The much celebrated hello world program in Flix:
+ +- Flix allows us to define our own data types and use pattern matching to take them apart: -
+Flix allows us to define our own data types and use pattern matching to take them apart:
-- Flix supports parametric polymorphism (generics) as the following example shows: -
+Flix supports parametric polymorphism (generics) as the following example shows:
-
- Note that type parameters may be omitted from function signatures, as shown in definition
- of map.
-
+ Note that type parameters may be omitted from function signatures, as shown in definition of{' '}
+ map.
+
- The concurrency model of Flix is inspired by Go. In Flix, processes communicate - via immutable message-passing over channels. -
++ The concurrency model of Flix is inspired by Go. In Flix, processes communicate via immutable + message-passing over channels. +
-- The following program spawns a new process to perform a (trivial) computation and then sends - the - result to the main process using a channel. -
++ The following program spawns a new process to perform a (trivial) computation and then sends the result to + the main process using a channel. +
-
- The powerful select expression can be used to choose the first element that
- becomes
- available from a collection of channels. The select expression can be used to implement many
- useful
- features, such as load balancing, producer-consumer patterns, and timeouts.
-
+ The powerful select expression can be used to choose the first element that becomes available
+ from a collection of channels. The select expression can be used to implement many useful features, such
+ as load balancing, producer-consumer patterns, and timeouts.
+
- A unique feature of Flix is its polymorphic effect system. The Flix type and effect system - cleanly separates pure and impure code. If an expression is pure then it always - evaluates to the same value and it cannot have a side-effect. If a function is pure then it - always evaluates to the same value when given the same arguments. -
++ A unique feature of Flix is its polymorphic effect system. The Flix type and effect system cleanly + separates pure and impure code. If an expression is pure then it always evaluates to the same value and it + cannot have a side-effect. If a function is pure then it always evaluates to the same value when given the + same arguments. +
-- We can write a pure function: -
+We can write a pure function:
-- And we can also write an impure function: -
+And we can also write an impure function:
-- We can also write a higher-order function that requires a pure function argument: -
++ We can also write a higher-order function that requires a pure function argument: +
-
- Here f is a pure function, because every function definition
- is implicitly marked as Pure in Flix.
-
- It is a compile-time error to call map with an impure function!
-
- A major challenge for type and effect systems is effect polymorphism. The problem is the
- following: for higher-order functions the effect of a function depends on the effects of its
- arguments. For example, if map is passed a pure function f then the
- expression List.map(f, 1 :: Nil) is pure. On the other hand, if map is passed
- an impure function g then the expression List.map(g, 1 :: Nil) is
- impure. The effect of map depends on the effect of its first argument: it is effect
- polymorphic.
-
- We can express such effect polymorphic function types in Flix. For example: -
- -
+ Here f is a pure function, because every function definition is implicitly marked as{' '}
+ Pure in Flix.
+
+
+ It is a compile-time error to call map with an impure function!
+
+
+ A major challenge for type and effect systems is effect polymorphism. The problem is the following: for
+ higher-order functions the effect of a function depends on the effects of its arguments. For example, if
+ map is passed a pure function f then the expression List.map(f, 1 :: Nil) is
+ pure. On the other hand, if map is passed an impure function g then the expression{' '}
+ List.map(g, 1 :: Nil) is impure. The effect of map depends on the effect of its first
+ argument: it is effect polymorphic.
+
+ We can express such effect polymorphic function types in Flix. For example: +
+ +
- Here the effect map depends on the effect of f (expressed with the
- effect parameter ef).
-
- The effect system of Flix is part of what makes the language functional-first: the - programmer can trust that a pure function behaves as a mathematical function. Most other - contemporary programming languages cannot offer such guarantees. -
- -- Another unique feature of Flix is its support for logic programming with first-class Datalog - constraints. Datalog is a simple, yet surprisingly powerful, declarative logic programming - language - particularly well-suited for recursive queries on graphs. In Flix, Datalog constraints can - be - embedded inside Flix programs as first-class values that can be stored in local - variables, - passed and returned from functions, and composed with other Datalog program values. In a - way, Flix - is a strongly-typed meta-programming language for Datalog. -
- -
+ Here the effect map depends on the effect of f (expressed with the effect
+ parameter ef).
+
+ The effect system of Flix is part of what makes the language functional-first: the programmer can trust + that a pure function behaves as a mathematical function. Most other contemporary programming languages + cannot offer such guarantees. +
+ ++ Another unique feature of Flix is its support for logic programming with first-class Datalog constraints. + Datalog is a simple, yet surprisingly powerful, declarative logic programming language particularly + well-suited for recursive queries on graphs. In Flix, Datalog constraints can be embedded inside{' '} + Flix programs as first-class values that can be stored in local variables, passed and returned from + functions, and composed with other Datalog program values. In a way, Flix is a strongly-typed + meta-programming language for Datalog. +
+ +- The solution to a Datalog program, its minimal model, is itself a Datalog program (i.e. a - set of - facts). Consequently, with first-class constraints, it becomes possible to construct - pipelines of - Datalog programs. -
- -- First-class Datalog constraints can also be polymorphic, as this example demonstrates: -
- -+ The solution to a Datalog program, its minimal model, is itself a Datalog program (i.e. a set of facts). + Consequently, with first-class constraints, it becomes possible to construct pipelines of Datalog + programs. +
+ +First-class Datalog constraints can also be polymorphic, as this example demonstrates:
+ +- We say that Flix is a next-generation programming language because it pioneers several new - features that are not found in any other contemporary programming language. However, - innovation is not a goal in itself; Flix also builds on decades of research in programming - language theory and relies on well-established theoretical foundations. -
- -- Flix comes with a polymorphic type and effect system. The effect system separates pure - and impure code. If an expression is pure then it always evaluates to the same value and it - cannot have a side-effect. If a function is pure then it always evaluates to the same value - when given the same arguments. -
- -
- Flix supports effect polymorphism which means that the effect of a higher-order
- function can depend on the effect of its function arguments. For example, the effect
- of List.map depends on the effect of the function passed to it. That is,
- if List.map is given a pure function then computation is pure, whereas if
- it is given an impure function then computation is impure. As an another example,
- the effect of >> (forward function composition) depends on both of
- its arguments: composition is only pure if both its function arguments are pure.
-
- The Flix type and effect system is fine-grained and expressive. It is fine-grained because - it precisely captures the purity of every expression and sub-expression. It is expressive - because it allows arbitrary boolean formulas to describe - the effect of an expression. For example, the system can express that a higher-order - function requires at most one impure function. -
- -- The Flix type and effect system supports type and effect inference. That is, explicit - type or effect annotations are never required for any program fragment. (However, as a - design choice, type and effect annotations are required for every top-level definition.) The - inference is complete which means that it never infers the wrong type or effect, i.e. - annotations are never required to guide the type checker. -
- -- The theoretical foundation of the Flix type and effect system is based on the Hindley-Milner - type system extended with boolean constraints. Type inference is supported by - an extension of Algorithm W with boolean unification. For more details, we refer to our - research papers. -
- -- Datalog is a simple, yet surprisingly powerful, declarative logic programming language. A - Datalog program is a collection of constraints. Each constraint is either a fact or a rule. - A Datalog rule is logic formula that allows us to derive new facts from existing facts. -
- -- Every Datalog program has a unique solution; its so-called minimal model. - The minimal model always exists and is always computable, i.e. evaluation of a Datalog - program always terminates with the same solution. In Datalog, unlike in Prolog, the order - of constraints and of clauses within a rule is immaterial. That is, a Datalog program - can be freely reordered without changing its meaning. -
- -- Datalog, unlike Prolog, is not Turing-complete: there are a programs that cannot be - expressed in Datalog. This is necessarily so, otherwise Datalog could not guarantee - termination. -
- -- Flix supports Datalog constraints as first-class values that can be passed around, - composed with other constraints, and solved. The solution (i.e. minimal model) of a - constraint set is another constraint set, hence it is possible to construct pipelines of - Datalog computations within a Flix program. -
- -- Flix can be thought of as a meta-programming language for Datalog. The Flix type system - and stratification algorithm guarantees the well-formedness of Datalog programs constructed - at run-time. Moreover, Flix significantly increases the expressive power of Datalog by - allowing guard expressions and expressions as head terms in Datalog rules. -
- -- 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). -
- - -+ We say that Flix is a next-generation programming language because it pioneers several new features that + are not found in any other contemporary programming language. However, innovation is not a goal in itself; + Flix also builds on decades of research in programming language theory and relies on well-established + theoretical foundations. +
+ ++ Flix comes with a polymorphic type and effect system. The effect system separates pure and impure code. If + an expression is pure then it always evaluates to the same value and it cannot have a side-effect. If a + function is pure then it always evaluates to the same value when given the same arguments. +
+ +
+ Flix supports effect polymorphism which means that the effect of a higher-order function can depend
+ on the effect of its function arguments. For example, the effect of List.map depends on the
+ effect of the function passed to it. That is, if List.map is given a pure function then
+ computation is pure, whereas if it is given an impure function then computation is impure. As an another
+ example, the effect of >> (forward function composition) depends on both of its
+ arguments: composition is only pure if both its function arguments are pure.
+
+ The Flix type and effect system is fine-grained and expressive. It is fine-grained because it precisely + captures the purity of every expression and sub-expression. It is expressive because it allows arbitrary + boolean formulas to describe the effect of an expression. For example, the system can express that a + higher-order function requires at most one impure function. +
+ ++ The Flix type and effect system supports type and effect inference. That is, explicit type or + effect annotations are never required for any program fragment. (However, as a design choice, type and + effect annotations are required for every top-level definition.) The inference is complete which + means that it never infers the wrong type or effect, i.e. annotations are never required to guide the type + checker. +
+ ++ The theoretical foundation of the Flix type and effect system is based on the Hindley-Milner type system + extended with boolean constraints. Type inference is supported by an extension of Algorithm W with boolean + unification. For more details, we refer to our research papers. +
+ ++ Datalog is a simple, yet surprisingly powerful, declarative logic programming language. A Datalog program + is a collection of constraints. Each constraint is either a fact or a rule. A Datalog rule is logic + formula that allows us to derive new facts from existing facts. +
+ ++ Every Datalog program has a unique solution; its so-called minimal model. The minimal model always + exists and is always computable, i.e. evaluation of a Datalog program always terminates with the same + solution. In Datalog, unlike in Prolog, the order of constraints and of clauses within a rule is + immaterial. That is, a Datalog program can be freely reordered without changing its meaning. +
+ ++ Datalog, unlike Prolog, is not Turing-complete: there are a programs that cannot be expressed in + Datalog. This is necessarily so, otherwise Datalog could not guarantee termination. +
+ ++ Flix supports Datalog constraints as first-class values that can be passed around, composed with + other constraints, and solved. The solution (i.e. minimal model) of a constraint set is another constraint + set, hence it is possible to construct pipelines of Datalog computations within a Flix program. +
+ ++ Flix can be thought of as a meta-programming language for Datalog. The Flix type system and stratification + algorithm guarantees the well-formedness of Datalog programs constructed at run-time. Moreover, Flix + significantly increases the expressive power of Datalog by allowing guard expressions and expressions as + head terms in Datalog rules. +
+ ++ 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). +
+ +- We maintain a blog about the development of the Flix programming language. - The blog is slow-moving since most of our writing bandwidth is directed towards - writing documentation and research papers. -
- -- The blog has a more personal style and its intended audience is primarily - programming language enthusiasts. -
+ render() { + return ( ++ We maintain a blog about the development of the Flix programming language. The blog is slow-moving + since most of our writing bandwidth is directed towards writing documentation and research papers. +
-+ The blog has a more personal style and its intended audience is primarily programming language + enthusiasts. +
+ ++ Flix is developed at Aarhus University, at + the University of Waterloo, and by a community of{' '} + open source contributors. +
-+ Flix is open-source and freely available under the{' '} + Apache 2.0 license. +
-- Flix is developed at Aarhus - University, at the University of Waterloo, and by - a community of open source - contributors. -
++ All source code is available on GitHub. We organize development + using GitHub issues and{' '} + Gitter. +
-- Flix is open-source and freely available under the Apache 2.0 license. -
++ If you are interested working on Flix, please feel free to reach out to us. We have already had several + positive experiences with mentorship and open source contributors. +
+ +- All source code is available on GitHub. +
- If you are interested working on Flix, please feel free to reach out to us. We have already - had several positive experiences with mentorship and open source contributors. -
- -- We are more than happy to mentor someone who is interested in working on compilers - and/or programming language design and wants to contribute to Flix. We have already - had several positive experiences working with open source - contributors. -
-- Aarhus University offers a talent track program for capable students that are in - their second or third year of studies and are interested in working on a research - project for up to one year as an extracurricular activity. -
-+ We are more than happy to mentor someone who is interested in working on compilers and/or programming + language design and wants to contribute to Flix. We have already had several positive experiences + working with open source contributors. +
+- If you are a bachelor or master student at Aarhus University you can - write your thesis on a topic related to Flix. -
-+ Aarhus University offers a talent track program for capable students that are in their second or third + year of studies and are interested in working on a research project for up to one year as an + extracurricular activity. +
+- If you want to become involved, send us a ping on Gitter, and we can have a chat about your - interests. + If you are a bachelor or master student at Aarhus University you can write your thesis on a topic + related to Flix.
-+ If you want to become involved, send us a ping on Gitter, and we + can have a chat about your interests. +
+ + ) + } } -export default Contribute; +export default Contribute diff --git a/src/page/Documentation.js b/src/page/Documentation.js index 5455589..f953e00 100644 --- a/src/page/Documentation.js +++ b/src/page/Documentation.js @@ -1,155 +1,136 @@ -import React, { Component } from 'react'; -import { Card, CardSubtitle, CardText, CardTitle, Col, Container, Row } from "reactstrap"; -import { Link } from "react-router-dom"; +import React, { Component } from 'react' +import { Card, CardSubtitle, CardText, CardTitle, Col, Container, Row } from 'reactstrap' +import { Link } from 'react-router-dom' -import { FaBookReader } from 'react-icons/fa'; -import { FaStream } from 'react-icons/fa'; -import { FaMicroblog } from 'react-icons/fa'; -import { FaGitter } from 'react-icons/fa'; -import { FaGithub } from 'react-icons/fa'; -import { FaRegLaughSquint } from 'react-icons/fa'; -import { MdSchool } from 'react-icons/md'; -import { GoGraph } from 'react-icons/go'; +import { FaBookReader } from 'react-icons/fa' +import { FaStream } from 'react-icons/fa' +import { FaMicroblog } from 'react-icons/fa' +import { FaGitter } from 'react-icons/fa' +import { FaGithub } from 'react-icons/fa' +import { FaRegLaughSquint } from 'react-icons/fa' +import { MdSchool } from 'react-icons/md' +import { GoGraph } from 'react-icons/go' class Documentation extends Component { + componentDidMount() { + document.title = 'Flix | Documentation' + } - componentDidMount() { - document.title = "Flix | Documentation"; - } + render() { + return ( +You may also be interested in these additional resources:
+ +- You may also be interested in these additional resources: -
- -- A collection of information that did not seem to fit in anywhere else. -
- -
- Yes, with the import mechanism.
-
- Flix borrows a lot of syntax from Scala, hence the two languages have a similar feel.
- We think Scala made many good design choices with respect to syntax, including:
- (a) the use of short keywords,
- (b) the x : T syntax for type annotations,
- (c) the List[Int32] syntax for type parameters, and
- (d) if, match, etc. as expressions.
-
- Other than syntax, the two languages are very different: Scala is object-oriented, Flix is - not. - Scala has sub-typing, Flix does not. The Scala type system is unsound and has imperfect - type inference, whereas the Flix type system is both sound and supports type inference. -
---interactive argument.
- - At the moment, Flix has not yet reached version 1.0. That means you will be an early - adopter, so you should expect for the language to evolve and be prepared for the rare - compiler bug. (The Flix compiler has 9,500 manually written tests and we - take correctness seriously.) -
- -- To write Flix programs, a solid background in functional programming is useful. That means - prior experience with OCaml, Haskell, Scala, or similar programming languages. -
-- We recommend that you start with a small offering to the Great Dreamer, the Sleeper of - R'lyeh, Cthulhu. And coffee. Lots of coffee. All kidding aside, the best place to start is - to look at the examples and to read the Programming - Flix book. -
- -- If you get stuck or need help feel free to reach out to us on Gitter. -
-- No, Flix is a full-blown functional programming language. -
- -- That said, Flix could be considered a meta-programming language for Datalog. -
-- Flix runs on the Java Virtual Machine (JVM) hence the performance of Flix is limited by the - performance of the JVM. Luckily, the JVM is a mature and performant virtual machine. Flix - uses monomorphization which eliminates boxing and in theory can make code execute faster - than ordinary Java / Kotlin / Scala code. However, Flix also features full tail call - elimination - which has some run-time performance cost. -
- -- Our goal to be faster than any interpreted language and within a few factors of - equivalent functional Scala code. -
-- To answer this question, it is important to distinguish between latency and throughput. -
- -- The Flix compiler runs on the JVM hence startup times can be expensive, i.e. the compiler - has high latency. However, once the JVM has warmed up the compiler is quite fast, i.e. has - high throughput. -
- -
- A simple experiment shows that the compiler runs about 20.0x times faster
- when warmed up compared to when cold. We estimate that Flix, when warmed up, compiles
- around 20,000 lines of code per second, which we believe to be faster than the
- Scala compiler, but slower than the Java compiler. We take compiler performance
- seriously and continuously track the performance of
- the compiler.
-
- Compiler throughput on an Intel i5-K8600k with 16GB of RAM. -
- -- Experimental results from the 30th of May 2020. -
- -| Threads | -Throughput (lines/sec) | -Ratio | -
|---|---|---|
| 1 | -9,673 | -1.0x | -
| 2 | -14,482 | -1.5x | -
| 3 | -17,100 | -1.8x | -
| 4 | -18,722 | -1.9x | -
| 5 | -20,118 | -2.1x | -
| 6 | -21,052 | -2.2x | -
- Flix will, by design, not support any of the following features: -
- -| Feature | -Reason | -
|---|---|
| Exceptions | -Exceptions have been used to deal with two types of errors that may arise during
- execution of a program: predictable errors (e.g. a file does not exist) and program
- bugs (e.g. stack overflow). Flix has no exceptions. Instead, all predictable errors
- should be encoded as partial functions (e.g. using Option) or as
- potentially error returning functions (e.g. using Result). We are still
- in the process of deciding how to handle program bugs.
- |
-
| Null Values | -
- Null, famously called Tony
- Hoare's billion dollar mistake, is simply a bad solution to the problem of how
- to represent the (potential) absence of a value. Instead, in Flix, you should use
- the Option data type.
- |
-
| Non-Total Functions | -
- The Flix standard library has been deliberately designed to avoid common
- programming mistakes. We want functions that are safe and have accurate type
- signatures. For example, unlike Scala or Haskell,
- the List.head function returns an Option since we cannot
- in general guarantee that a list is non-empty.
- |
-
| Silent Coercions | -- Implicit coercions between data types (e.g. between booleans and other values or - between enums and integers) is a rich source of programming mistakes. In Flix, - no type is ever converted to another type without explicit instruction from the - programmer. - | -
| No Code Before Main | -- In Flix, no code is ever executed before main. Flix has no static initializers (or - similar constructs) which are difficult to reason about, error-prone, and often lead - to buggy code. - | -
| Equality and Assignment Confusion | -
- In Flix, the equality test operator (==) is different from the
- assignment operator (:=) which is different from the equality sign
- (=) used in definitions and let-bindings. Flix has been designed such
- that programs that mistake one for the other is unlikely to compile.
- |
-
| Undefined Behavior | -Undefined behavior is frequently the cause of program bugs and - vulnerabilities. We want every Flix program to have a well-defined semantics. - | -
- This list was partially inspired by the blog post things rust shipped without. -
-- The following design choices may be considered controversial by some: -
- -- Flix is a research project carried out by faculty and students at Aarhus University and the University - of Waterloo. -
- -- Flix is partially supported by a grant of 2,500,000 DKK from the Independent - Research Fund of Denmark. -
-- The latest compiler version and the website is not always in sync, hence occasionally some - examples may stop to work. Feel free to open a bug report if this happens. -
- -- Occasionally a mischievous visitor will crash the online editor (or rather the virtual - machine on which the compiler runs). We usually discover and fix this within a few days. -
-- Yes, no programming language developed outside of those four corporations have ever been - successful. See also C, C++, Java, Python, PHP, MatLab, Perl, R, Ruby, Scala, ... -
- -- That said, if you work for a company and would like to help sponsor Flix, please feel free - to reach out to us :) -
-- Do we really need safer airplanes? Do we really need electric cars? Do we - really need more ergonomic chairs? -
- -- I mean, after all, we already have airplanes, cars, and chairs! -
- -- We build new programming languages and we conduct research on programming language design - because we want to offer developers better tools to write programs. We want to make - it simpler, safer, and faster to write correct programs. -
- -- And we want to increase developer happiness. It should be a pleasure to use Flix! -
-- The Flix syntax is based on keywords except when there is a - clearly established historical precedent for using a symbol. For example: -
- -x and a list xs is written as x
- :: xs.
- _ denotes a wildcard (or an unused variable).<- c reads a value from a channel whereas c <-
- v writes a value to a channel.
- :- denotes logical implication in Datalog rules.A collection of information that did not seem to fit in anywhere else.
+ +
+ Yes, with the import mechanism.
+
+ Flix borrows a lot of syntax from Scala, hence the two languages have a similar feel. We think Scala made
+ many good design choices with respect to syntax, including: (a) the use of short keywords, (b) the{' '}
+ x : T syntax for type annotations, (c) the List[Int32] syntax for type
+ parameters, and (d) if, match, etc. as expressions.
+
+ Other than syntax, the two languages are very different: Scala is object-oriented, Flix is not. Scala has + sub-typing, Flix does not. The Scala type system is unsound and has imperfect type inference, whereas the + Flix type system is both sound and supports type inference. +
+--interactive argument.
+ + At the moment, Flix has not yet reached version 1.0. That means you will be an early adopter, so you + should expect for the language to evolve and be prepared for the rare compiler bug. (The Flix compiler has + 9,500 manually written tests and we take correctness seriously.) +
+ ++ To write Flix programs, a solid background in functional programming is useful. That means prior + experience with OCaml, Haskell, Scala, or similar programming languages. +
++ We recommend that you start with a small offering to the Great Dreamer, the Sleeper of R'lyeh, Cthulhu. + And coffee. Lots of coffee. All kidding aside, the best place to start is to look at the examples and to + read the Programming Flix book. +
+ +If you get stuck or need help feel free to reach out to us on Gitter.
+No, Flix is a full-blown functional programming language.
+ +That said, Flix could be considered a meta-programming language for Datalog.
++ Flix runs on the Java Virtual Machine (JVM) hence the performance of Flix is limited by the performance of + the JVM. Luckily, the JVM is a mature and performant virtual machine. Flix uses monomorphization which + eliminates boxing and in theory can make code execute faster than ordinary Java / Kotlin / Scala code. + However, Flix also features full tail call elimination which has some run-time performance cost. +
+ ++ Our goal to be faster than any interpreted language and within a few factors of equivalent functional + Scala code. +
++ To answer this question, it is important to distinguish between{' '} + latency and{' '} + throughput. +
+ ++ The Flix compiler runs on the JVM hence startup times can be expensive, i.e. the compiler has high + latency. However, once the JVM has warmed up the compiler is quite fast, i.e. has high throughput. +
+ +
+ A simple experiment shows that the compiler runs about 20.0x times faster when warmed up
+ compared to when cold. We estimate that Flix, when warmed up, compiles around 20,000 lines of
+ code per second, which we believe to be faster than the Scala compiler, but slower than the Java compiler.
+ We take compiler performance seriously and continuously track the{' '}
+ performance of the compiler.
+
Compiler throughput on an Intel i5-K8600k with 16GB of RAM.
+ +Experimental results from the 30th of May 2020.
+ +| + Threads + | +Throughput (lines/sec) | +Ratio | +
|---|---|---|
| 1 | +9,673 | +1.0x | +
| 2 | +14,482 | +1.5x | +
| 3 | +17,100 | +1.8x | +
| 4 | +18,722 | +1.9x | +
| 5 | +20,118 | +2.1x | +
| 6 | +21,052 | +2.2x | +
+ Flix will, by design, not support any of the following features: +
+ +| Feature | +Reason | +
|---|---|
| Exceptions | +
+ Exceptions have been used to deal with two types of errors that may arise during execution of a
+ program: predictable errors (e.g. a file does not exist) and program bugs (e.g. stack overflow).
+ Flix has no exceptions. Instead, all predictable errors should be encoded as partial functions (e.g.
+ using Option) or as potentially error returning functions (e.g. using{' '}
+ Result). We are still in the process of deciding how to handle program bugs.
+ |
+
| Null Values | +
+ Null, famously called{' '}
+ Tony Hoare's billion dollar mistake, is
+ simply a bad solution to the problem of how to represent the (potential) absence of a value.
+ Instead, in Flix, you should use the Option data type.
+ |
+
| Non-Total Functions | +
+ The Flix standard library has been deliberately designed to avoid common programming mistakes. We
+ want functions that are safe and have accurate type signatures. For example, unlike Scala or
+ Haskell, the List.head function returns an Option since we cannot in
+ general guarantee that a list is non-empty.
+ |
+
| Silent Coercions | ++ Implicit coercions between data types (e.g. between booleans and other values or between enums and + integers) is a rich source of programming mistakes. In Flix, no type is ever converted to another + type without explicit instruction from the programmer. + | +
| No Code Before Main | ++ In Flix, no code is ever executed before main. Flix has no static initializers (or similar + constructs) which are difficult to reason about, error-prone, and often lead to buggy code. + | +
| Equality and Assignment Confusion | +
+ In Flix, the equality test operator (==) is different from the assignment operator (
+ :=) which is different from the equality sign (=) used in definitions and
+ let-bindings. Flix has been designed such that programs that mistake one for the other is unlikely
+ to compile.
+ |
+
| Undefined Behavior | ++ Undefined behavior is frequently the cause of program bugs and vulnerabilities. We want every Flix + program to have a well-defined semantics. + | +
+ This list was partially inspired by the blog post{' '} + things rust shipped without. +
+The following design choices may be considered controversial by some:
+ ++ Flix is a research project carried out by faculty and students at{' '} + Aarhus University and the{' '} + University of Waterloo. +
+ ++ Flix is partially supported by a grant of 2,500,000 DKK from the{' '} + Independent Research Fund of Denmark. +
++ The latest compiler version and the website is not always in sync, hence occasionally some examples may + stop to work. Feel free to open a bug report if this happens. +
+ ++ Occasionally a mischievous visitor will crash the online editor (or rather the virtual machine on which + the compiler runs). We usually discover and fix this within a few days. +
++ Yes, no programming language developed outside of those four corporations have ever been successful. See + also C, C++, Java, Python, PHP, MatLab, Perl, R, Ruby, Scala, ... +
+ ++ That said, if you work for a company and would like to help sponsor Flix, please feel free to reach out to + us :) +
++ Do we really need safer airplanes? Do we really need electric cars?{' '} + Do we really need more ergonomic chairs? +
+ +I mean, after all, we already have airplanes, cars, and chairs!
+ ++ We build new programming languages and we conduct research on programming language design because we want + to offer developers better tools to write programs. We want to make it simpler, safer + , and faster to write correct programs. +
+ +And we want to increase developer happiness. It should be a pleasure to use Flix!
++ The Flix syntax is based on keywords except when there is a + clearly established historical precedent for using a symbol. For example: +
+ +x and a list xs is written as x :: xs.
+ _ denotes a wildcard (or an unused variable).
+ <- c reads a value from a channel whereas c <- v writes a
+ value to a channel.
+ :- denotes logical implication in Datalog rules.
+ + You can try Flix online at play.flix.dev. +
+ +- You can try Flix online at play.flix.dev. -
- -+ Or you can install Flix in Visual Studio Code: +
-- Or you can install Flix in Visual Studio - Code: -
+-
java
- -version.
- flix.jar) at https://github.com/flix/flix/releases/latest.
- mkdir flixproject) and place the
- downloaded Flix JAR (flix.jar) into that folder.
- cd flixproject) and run java
- -jar flix.jar init to create an empty Flix project.
- java -jar flix.jar run to compile and run the project.main function (located
- in src/Main.flix).
- +
java -version.
+ flix.jar) at{' '}
+
+ https://github.com/flix/flix/releases/latest
+
+ .
+ mkdir flixproject) and place the downloaded Flix JAR (
+ flix.jar) into that folder.
+ cd flixproject) and run{' '}
+ java -jar flix.jar init to create an empty Flix project.
+ java -jar flix.jar run to compile and run the project.
+ main function (located in{' '}
+ src/Main.flix).
+ - Flix is a principled functional, imperative, and logic programming language - developed at Aarhus University, at the University of Waterloo, and by a community of open source contributors. -
- -- Flix is inspired by OCaml and Haskell with ideas from Rust and Scala. Flix looks like - Scala, but its type system is based on Hindley-Milner. Two unique features - of Flix are its polymorphic effect system and its support for first-class Datalog - constraints. -
- -- Flix compiles to JVM bytecode, runs on the Java Virtual Machine, and supports full tail call - elimination. A VSCode plugin for Flix is available. -
- - - - -- Flix aims to offer a unique combination of - features that no other programming language offers, including: algebraic - data types and pattern matching (like Haskell, OCaml), extensible records (like Elm), type classes (like Haskell, Rust), higher-kinded types (like Haskell), typematch (like Scala), type inference (like Haskell, OCaml), structured channel and process-based concurrency (like - Go), a polymorphic effect system (a unique - feature), region-based local mutation (a unique - feature), purity reflection (a unique - feature), first-class Datalog constraints (a unique - feature), - and compilation to JVM bytecode (like Scala). -
- - -- Algebraic data types and pattern matching are the bread-and-butter of functional - programming and are supported by Flix with minimal fuss. -
-+ Flix is a principled functional, imperative, and logic programming language developed at{' '} + Aarhus University, at the{' '} + University of Waterloo, and by a community of{' '} + open source contributors. +
+ ++ Flix is inspired by OCaml and Haskell with ideas from Rust and Scala. Flix looks like Scala, but its type + system is based on Hindley-Milner. Two unique features of Flix are its polymorphic effect system and its + support for first-class Datalog constraints. +
+ ++ Flix compiles to JVM bytecode, runs on the Java Virtual Machine, and supports full tail call elimination. + A VSCode plugin for Flix is available. +
+ + + ++ Flix aims to offer a unique combination of features{' '} + that no other programming language offers, including:{' '} + algebraic data types and pattern matching (like Haskell, OCaml),{' '} + extensible records (like Elm),{' '} + type classes (like Haskell, Rust),{' '} + higher-kinded types (like Haskell),{' '} + typematch (like Scala),{' '} + type inference (like Haskell, OCaml),{' '} + structured channel and process-based concurrency (like Go),{' '} + a polymorphic effect system (a unique feature),{' '} + region-based local mutation (a unique feature),{' '} + purity reflection (a unique feature),{' '} + first-class Datalog constraints (a unique feature), + and compilation to JVM bytecode (like Scala). +
+ ++ Algebraic data types and pattern matching are the bread-and-butter of functional programming and are + supported by Flix with minimal fuss. +
+- Flix has built-in support for tuples and records. -
- -- Records use structural typing and are extensible. -
-- Flix precisely tracks the purity of every expression in a program. -
- -- The Flix compiler provides an ironclad guarantee that if an expression is pure - then it cannot have side-effects and it is referentially transparent. -
-Flix has built-in support for tuples and records.
+ +Records use structural typing and are extensible.
+Flix precisely tracks the purity of every expression in a program.
+ ++ The Flix compiler provides an ironclad guarantee that if an expression is pure then it cannot have + side-effects and it is referentially transparent. +
+- Flix is able to track purity through higher-order effect polymorphic functions. -
- -
- For example, Flix knows that the purity of List.map depends on the
- purity of its function argument f.
-
- Flix supports region-based local mutation, which makes it possible to - implement pure functions that internally uses mutable state and - destructive operations, as long as these operations are confined to the region. -
- -- We can use local mutation when it is more natural to write a function using - mutable data and in a familiar imperative-style while still remaining pure - to the outside world. -
- -- We can also use local mutation when it is more efficient to use mutable - data structures, e.g. when implementing a sorting algorithm. -
-Flix is able to track purity through higher-order effect polymorphic functions.
+ +
+ For example, Flix knows that the purity of List.map depends on the purity of its
+ function argument f.
+
+ Flix supports region-based local mutation, which makes it possible to implement pure{' '} + functions that internally uses mutable state and destructive operations, as long as these operations + are confined to the region. +
+ ++ We can use local mutation when it is more natural to write a function using mutable data and in a + familiar imperative-style while still remaining pure to the outside world. +
+ ++ We can also use local mutation when it is more efficient to use mutable data structures, e.g. when + implementing a sorting algorithm. +
+- Flix supports a meta-programming construct that enables higher-order functions - to inspect the purity of a function argument and use that information to vary - their behavior. -
- -
- For example, the DelayList.map function varies its behavior between
- eager and lazy evaluation depending on the purity of its function argument.
-
- We can exploit purity reflection to selectively use lazy or parallel - evaluation inside a library without changing the semantics from the - point-of-view of the clients. -
-- Flix uses type classes to abstract over types that support a common set of - operations. -
-
- For example, the Eq type class captures the notion of equality
- and is used throughout the standard library.
-
+ Flix supports a meta-programming construct that enables higher-order functions to inspect the purity + of a function argument and use that information to vary their behavior. +
+ +
+ For example, the DelayList.map function varies its behavior between eager and lazy
+ evaluation depending on the purity of its function argument.
+
+ We can exploit purity reflection to selectively use lazy or parallel evaluation inside a library + without changing the semantics from the point-of-view of the clients. +
+Flix uses type classes to abstract over types that support a common set of operations.
+
+ For example, the Eq type class captures the notion of equality and is used throughout
+ the standard library.
+
- Flix supports higher-kinded types making it possible to abstract over type
- constructors. For example,
- both Option and List implement Foldable.
-
- The Flix standard library ships with many common type classes, such
- as Monoid, Functor, and Foldable.
-
- Flix supports a monadic forM-yield construct similar to Scala's
- for-comprehensions and Haskell's do notation.
- The forM construct is syntactic sugar for uses
- of point and flatMap (which are provided by the Monad
- type class).
-
+ Flix supports higher-kinded types making it possible to abstract over type constructors. For
+ example, both Option and List implement Foldable.
+
+ The Flix standard library ships with many common type classes, such as Monoid,{' '}
+ Functor, and Foldable.
+
+ Flix supports a monadic forM-yield construct similar to Scala's
+ for-comprehensions and Haskell's do notation. The forM{' '}
+ construct is syntactic sugar for uses of point and flatMap (which are
+ provided by the Monad type class).
+
- In addition to the monadic forM expression, Flix supports an
- applicative forA expression that builds on
- the Applicative type class. The forA construct makes
- it simple to write error-handling code which uses the Validation[e,
- t] data type.
-
- Another unique feature of Flix is its embedded Datalog support. Datalog, a - powerful logic programming language in its own right, makes it simple and - elegant to express many fixpoint problems (including various graph reachability - problems): -
- -
+ In addition to the monadic forM expression, Flix supports an applicative{' '}
+ forA expression that builds on the Applicative type class. The{' '}
+ forA construct makes it simple to write error-handling code which uses the{' '}
+ Validation[e, t] data type.
+
+ Another unique feature of Flix is its embedded Datalog support. Datalog, a powerful logic + programming language in its own right, makes it simple and elegant to express many fixpoint problems + (including various graph reachability problems): +
+ +- Datalog constraints are first-class which means that they may be passed - to and returned from functions, stored in data structures, composed with other - Datalog constraints, and solved. This makes it possible to express families of - Datalog programs. -
-- Flix supports Datalog constraints enriched with lattice semantics. -
- -- The program on the right computes the delivery date for a collection of - parts. Each part is assembled from a collection of sub-components with various - delivery dates. For example, a car depends on a chassis and an engine. To build - a car, we need to wait for the chassis and engine to assembled and then we can - assemble the car itself. -
- -- Note that parts may depend on sub-components that themselves may depend on other - sub-components. In other words, the problem is recursive. -
- -- Datalog constraints enriched with lattice semantics is one of the more - advanced features of Flix and requires some background knowledge of lattice - theory and fixpoints. -
-+ Datalog constraints are first-class which means that they may be passed to and returned from + functions, stored in data structures, composed with other Datalog constraints, and solved. This + makes it possible to express families of Datalog programs. +
+ + + + +Flix supports Datalog constraints enriched with lattice semantics.
+ ++ The program on the right computes the delivery date for a collection of parts. Each part is + assembled from a collection of sub-components with various delivery dates. For example, a car + depends on a chassis and an engine. To build a car, we need to wait for the chassis and engine to + assembled and then we can assemble the car itself. +
+ ++ Note that parts may depend on sub-components that themselves may depend on other sub-components. In + other words, the problem is recursive. +
+ ++ Datalog constraints enriched with lattice semantics is one of the more advanced features of Flix and + requires some background knowledge of lattice theory and fixpoints. +
+- The Flix compiler integrates with Visual Studio Code providing a richer development - experience: -
- -- We kindly thank EJ Technologies for providing - us with JProfiler and JetBrains for providing us with IntelliJ IDEA. -
- -The Flix compiler integrates with Visual Studio Code providing a richer development experience:
+ ++ We kindly thank EJ Technologies for providing us with{' '} + JProfiler and{' '} + JetBrains for providing us with{' '} + IntelliJ IDEA. +
+ +- Interested in programming language research? - Want to work on compilers? - Want to work on Flix? -
- -- Then join us for a research internship at Aarhus University in Denmark! -
- -
- To apply, send an email to magnusm at cs dot au dot dk with a bit of
- information about yourself.
-
- A typical research internship lasts 6-8 weeks in the summer period (but other times of year - may also be possible). -
- -- Aarhus University will reimburse travel and visa costs for coming to Denmark. - In addition, it is possible to apply for a small stipend to help cover housing and living - expenses. -
- -- To apply, you should be enrolled in a bachelor's or master's degree programme at an accredited - university. You should have taken one or two courses on programming languages and on compilers - (exceptions can be made for especially talented students.) -
- -- If you have questions, feel free to head over to Gitter and talk to us. -
- -+ Interested in programming language research? Want to work on compilers? Want to work on Flix? +
+ +Then join us for a research internship at Aarhus University in Denmark!
+ +
+ To apply, send an email to magnusm at cs dot au dot dk with a bit of information about
+ yourself.
+
+ A typical research internship lasts 6-8 weeks in the summer period (but other times of year may also be + possible). +
+ ++ Aarhus University will reimburse travel and visa costs for coming to Denmark. In addition, it is possible + to apply for a small stipend to help cover housing and living expenses. +
+ ++ To apply, you should be enrolled in a bachelor's or master's degree programme at an accredited university. + You should have taken one or two courses on programming languages and on compilers (exceptions can be made + for especially talented students.) +
+ ++ If you have questions, feel free to head over to Gitter and + talk to us. +
+ +- Koan — A paradox to be meditated upon that is used to train Zen Buddhist monks - to abandon ultimate dependence on reason and to force them into gaining sudden intuitive - enlightenment. -
- -+ Koan — A paradox to be meditated upon that is used to train Zen Buddhist monks to abandon + ultimate dependence on reason and to force them into gaining sudden intuitive enlightenment. +
+ +- An orphaned process has no parent or has init (pid 1) as its parent. A zombie - process is dead, but its parent is still alive. -
++ An orphaned process has no parent or has init (pid 1) as its parent. A zombie process{' '} + is dead, but its parent is still alive. +
-- We believe that the development of a programming language should follow a set of principles. - That is, when a design decision is made there should exist some rationale for why that - decision was made. By outlining these principles, as we develop Flix, we hope to keep ourselves - honest and to communicate the kind of language Flix aspires to be. -
- -- Many of these ideas and principles come from languages that have inspired Flix, including Ada, Elm, - F#, Go, Haskell, OCaml, Rust, and Scala. -
- -- Update: The Flix Principles has been published in a paper at Onward! '22. Read it here: The Principles of the Flix Programming - Language. -
- -List.map is def map[a,
- b](f: a -{'>'} b, xs: List[a]): List[b], we can use type parameter elision to
- write it
- simply as: def map(f: a -{'>'} b, xs: List[a]): List[b] omitting the type
- arguments.
- def, let, law,
- rel, but not for commonly established concepts: if ... else
- and match.
- f(a, b, c) whereas a type application
- is written as f[a, b, c].
- x -> x + 1 whereas a function type
- is written as Int -> Int.
- (true, 12345) whereas a tuple type
- is written as (Bool, Int).
- [0-99].
- main is the entry point of a program.
- No (user-defined) code is ever executed before main.
- No static initializers, no static fields. No class loaders. Main is always first.
- This makes it easy to reason about startup behavior.
- Option, List, Set,
- and Map, but for these it offers a comprehensive collection of functionality.
- For example, the standard library has more than 65 functions for working with lists.
- We want the standard library to offer a common set of abstractions which are usable
- by most programs, but not much else.
- null value. The null value is now widely considered a
- mistake and languages such as C#, Dart, Kotlin and Scala are scrambling to adopt mechanisms to
- ensure non-nullness.
- In Flix, we adopt the standard solution from functional languages which is to represent
- the absence of a value using the Option type. This solution is simple to
- understand, works well, and guarantees the absence of dreaded NullPointerExceptions.
- Map.filter and Map.filterWithKey, for functions that share
- similar functionality.
- Celsius instead of Int) or alternatively (ii) using record types
- which can be used to emulate the same functionality and works with higher-order functions.
- - Compiler messages are the main interface between Flix and programmers. We should invest into it. -
- -- The rule states that 80% of the time a developer will need minimal information to understand - a compiler message. Most likely the developer will already have seen the specific - error message hundreds of times before. But 20% of the time, the developer will - never have seen the message before and will need more information. -
- -- Flix compiler messages should accommodate both scenarios. -
-- A compiler message consists of three components: - -
- A message should be crisp, concise, and clear.
- The language should be friendly or neutral. An error message should not blame
- the programmer. For example, we should prefer Unexpected foo over Illegal
- foo, since the latter implies that the programmer did something wrong.
-
- The error message: Duplicate definition: 'foo' is better than the error
- message: The definition 'foo' is defined twice because in the former the
- programmer only has to scan the first word to understand what is wrong.
-
- When relevant, a Flix compiler error should explain how Flix differs from other languages - and explain how the specific problem can be solved in Flix. -
-- A type class is conceptually a function from a type to a set of lawful - operations (called signatures) on values of that type. -
- -
- For example, the Eq type class takes a type and returns
- the eq and neq functions where eq must be reflexive,
- symmetric, and transitive, and neq must be
- the negation of eq.
-
- Every type class must specify a collection of laws that instances of the type - class must satisfy. If a type class does not specify any laws it is lawless. -
- -- Here are some examples of lawful and lawless type classes: - -
Eq, Order, Functor, Foldable.
- FromString, ToString, Add.- A type class is lawful if every signature of the class is used in at least one law. -
- -- Note: Laws are not checked by the compiler – that is an undecidable - problem – but they may be used in a future SmallCheck / QuickCheck library. -
- -
- A sub-class (i.e. a type class A that refines a type class B) must
- specify additional laws that its instances must satisfy.
-
- For example, the Applicative type class extends the Functor type
- class with additional operations and laws.
-
sealed in which case no further instances, other than
- those in the same namespace, can be defined. A sealed type class can be used when the programmer
- wants to maintain tight control over what instances should be permitted.
- - The Flix compiler ensures that the selection of type class instances is always unambiguous. -
- -- In the future, we may allow a limited form of overlapping instances. -
-- Every type class belongs to a namespace. Hence it is possible to define multiple operations - with the same name, as long as they belong to type classes in different namespaces. -
- -- Every type class also defines a companion namespace which typically holds functions - that are not part of the type class, but nevertheless are related to the functionality of - the type class. -
-- Type classes may provide default implementations of functions. -
- -
- For example, the Foldable type class may provide default function
- implementations, e.g. count and length, based on
- the foldLeft and foldRight signatures defined in that class.
-
- A default implementation can always be overriden by a specific type class instance. - For example, to provide a more efficient version. -
-override keyword. This ensures that there are no dangling overrides,
- i.e. functions definitions that do not match any signature of the type class.
- Array and MutSet support
- the map operation. Flix, being functional-first, reserves functional names for
- functional operations. Across the standard library map has the same name and the
- same type signature.
- Array.reverse(a) returns a new array with the elements
- of a in reverse
- order, whereas Array.reverse!(a) destructively re-orders the elements
- of a. Note: This principle applies to destructive operations that operate on data
- structures, not to impure functions in general, e.g. Console.printLine.
- Array.reverse and Array.reverse! share the
- same name. On the other hand, Array.transform! is
- called transform! and not map! because its type signature is
- dissimilar to map (i.e. map works on functions of type a -{'>'} b, but transform
- requires functions of type a -{'>'} a.)
- + We believe that the development of a programming language should follow a set of principles. That is, when a + design decision is made there should exist some rationale for why that decision was made. By outlining these + principles, as we develop Flix, we hope to keep ourselves honest and to communicate the kind of language Flix + aspires to be. +
+ ++ Many of these ideas and principles come from languages that have inspired Flix, including Ada, Elm, F#, Go, + Haskell, OCaml, Rust, and Scala. +
+ ++ Update: The Flix Principles has been published in a paper at Onward! '22. Read it here:{' '} + The Principles of the Flix Programming Language. +
+ +List.map is{' '}
+ def map[a, b](f: a -{'>'} b, xs: List[a]): List[b], we can use type parameter elision to
+ write it simply as: def map(f: a -{'>'} b, xs: List[a]): List[b] omitting the type arguments.
+ def, let, law,rel, but not for commonly established
+ concepts: if ... else
+ and match.
+ f(a, b, c) whereas a type application is written as{' '}
+ f[a, b, c].
+ x -> x + 1 whereas a function type is written as{' '}
+ Int -> Int.
+ (true, 12345) whereas a tuple type is written as{' '}
+ (Bool, Int).
+ [0-99].
+ main is the entry point of a program. No (user-defined) code is ever executed before{' '}
+ main. No static initializers, no static fields. No class loaders. Main is always first. This
+ makes it easy to reason about startup behavior.
+ Option, List,{' '}
+ Set, and Map, but for these it offers a comprehensive collection of functionality.
+ For example, the standard library has more than 65 functions for working with lists. We want the standard
+ library to offer a common set of abstractions which are usable by most programs, but not much else.
+ null value. The null value is now widely considered a mistake and
+ languages such as C#, Dart, Kotlin and Scala are scrambling to adopt mechanisms to ensure non-nullness. In
+ Flix, we adopt the standard solution from functional languages which is to represent the absence of a value
+ using the Option type. This solution is simple to understand, works well, and guarantees the
+ absence of dreaded NullPointerExceptions.
+ Map.filter and Map.filterWithKey, for
+ functions that share similar functionality.
+ Celsius instead of Int) or
+ alternatively (ii) using record types which can be used to emulate the same functionality and works with
+ higher-order functions.
+ Compiler messages are the main interface between Flix and programmers. We should invest into it.
+ ++ The rule states that 80% of the time a developer will need minimal information to understand a compiler + message. Most likely the developer will already have seen the specific error message hundreds of times + before. But 20% of the time, the developer will never have seen the message before and will need more + information. +
+ +Flix compiler messages should accommodate both scenarios.
++ A compiler message consists of three components: +
+ A message should be crisp, concise, and clear. The language should be friendly or
+ neutral. An error message should not blame the programmer. For example, we should prefer{' '}
+ Unexpected foo over Illegal foo, since the latter implies that the programmer
+ did something wrong.
+
+ The error message: Duplicate definition: 'foo' is better than the error message:{' '}
+ The definition 'foo' is defined twice because in the former the programmer only has to scan
+ the first word to understand what is wrong.
+
+ When relevant, a Flix compiler error should explain how Flix differs from other languages and explain how + the specific problem can be solved in Flix. +
++ A type class is conceptually a function from a type to a set of lawful operations (called + signatures) on values of that type. +
+ +
+ For example, the Eq type class takes a type and returns the eq and{' '}
+ neq functions where eq must be reflexive, symmetric, and transitive, and{' '}
+ neq must be the negation of eq.
+
+ Every type class must specify a collection of laws that instances of the type class must satisfy. If a + type class does not specify any laws it is lawless. +
+ ++ Here are some examples of lawful and lawless type classes: +
Eq, Order, Functor, Foldable.
+ FromString, ToString, Add.
+ A type class is lawful if every signature of the class is used in at least one law.
+ ++ Note: Laws are not checked by the compiler – that is an undecidable problem – but they may be + used in a future SmallCheck / QuickCheck library. +
+
+ A sub-class (i.e. a type class A that refines a type class B) must specify
+ additional laws that its instances must satisfy.
+
+ For example, the Applicative type class extends the Functor type class with
+ additional operations and laws.
+
sealed in which case no further instances, other than those in the
+ same namespace, can be defined. A sealed type class can be used when the programmer wants to maintain tight
+ control over what instances should be permitted.
+ The Flix compiler ensures that the selection of type class instances is always unambiguous.
+ +In the future, we may allow a limited form of overlapping instances.
++ Every type class belongs to a namespace. Hence it is possible to define multiple operations with the same + name, as long as they belong to type classes in different namespaces. +
+ ++ Every type class also defines a companion namespace which typically holds functions that are not + part of the type class, but nevertheless are related to the functionality of the type class. +
+Type classes may provide default implementations of functions.
+ +
+ For example, the Foldable type class may provide default function implementations, e.g.{' '}
+ count and length, based on the foldLeft and foldRight{' '}
+ signatures defined in that class.
+
+ A default implementation can always be overriden by a specific type class instance. For example, to + provide a more efficient version. +
+override keyword. This ensures that there are no dangling overrides, i.e. functions definitions
+ that do not match any signature of the type class.
+ Array and MutSet support the map operation. Flix, being
+ functional-first, reserves functional names for functional operations. Across the standard library{' '}
+ map has the same name and the same type signature.
+ Array.reverse(a) returns a new array with the elements of a in reverse order,
+ whereas Array.reverse!(a) destructively re-orders the elements of a. Note: This
+ principle applies to destructive operations that operate on data structures, not to impure functions in
+ general, e.g. Console.printLine.
+ Array.reverse and Array.reverse!{' '}
+ share the same name. On the other hand, Array.transform! is called transform! and
+ not map! because its type signature is dissimilar to map (i.e. map works on functions of type{' '}
+ a -{'>'} b, but transform requires functions of type a -{'>'} a.)
+ - Research on Flix takes place at Aarhus - University and the University of Waterloo. -
- -- Below is a selection of research papers published on Flix: -
- -+ Research on Flix takes place at{' '} + Aarhus University and the{' '} + University of Waterloo. +
+ +Below is a selection of research papers published on Flix:
+ +- Posted January 2020 by Magnus Madsen. -
- -- Inspired by the blog post Design Flaws in - Futhark, I decided to take stock and reflect on some of the design flaws that I believe - we made during the development of the Flix programming language. I went through old - Github issues and pull requests to discover some of the challenging issues that we have been - or still are struggling with. I will classify the design flaws into four categories: - (i) design flaws that still plague the Flix language, (ii) design flaws that have been - fixed, (iii) poor designs that were thankfully never implemented, and finally (iv) design - choices where the jury is still out. -
- -- I want to emphasize that language design and implementation is a herculean task and that - there are features planned for Flix which have not yet been implemented. The lack of a - specific feature is not a design flaw, but rather a question of when we can get around to - it. -
- -- The following design flaws are still present in Flix. Hopefully some day they will be fixed. -
- -
- Flix supports the switch expression:
-
+ Posted January 2020 by Magnus Madsen. +
+ ++ Inspired by the blog post{' '} + + Design Flaws in Futhark + + , I decided to take stock and reflect on some of the design flaws that I believe we made during the + development of the Flix programming language. I went through old Github issues and pull requests to + discover some of the challenging issues that we have been or still are struggling with. I will classify + the design flaws into four categories: (i) design flaws that still plague the Flix language, (ii) design + flaws that have been fixed, (iii) poor designs that were thankfully never implemented, and finally (iv) + design choices where the jury is still out. +
+ ++ I want to emphasize that language design and implementation is a herculean task and that there are + features planned for Flix which have not yet been implemented. The lack of a specific feature is not a + design flaw, but rather a question of when we can get around to it. +
+ +The following design flaws are still present in Flix. Hopefully some day they will be fixed.
+ +
+ Flix supports the switch expression:
+
- where the boolean expressions cond1, cond2,
- and cond3 are evaluated from top to bottom until one of them returns true and
- then its associated body expression is evaluated. The idea, quite simply, is to have a
- control-flow structure that visually resembles an ordinary pattern match, but where there is
- no match value.
-
- In hind-sight, the switch expression is nothing more than a
- glorified if-then-else-if construct that does not carry its own weight.
- It is an expenditure on the complexity and strangeness budget that offers almost no gain
- over using plain if-then-else-if. Moreover, it is error-prone, because it lacks
- and explicit else branch in case none of the conditions evaluate to true. We
- plan to remove it in future versions of Flix.
-
- Like most contemporary languages, Flix uses + for string concatenation. While
- this is an uncontroversial design choice, it does not make much sense since strings are not
- commutative, e.g. "abc" + "def" is not the same as "def" +
- "abc". A better alternative would be to use ++ as in Haskell. However, I
- believe an even better design choice would be to forgo string concatenation and
- instead rely entirely on string interpolation. String interpolation is a much more powerful
- and elegant solution to the problem of building complex strings.
-
- The following design flaws have been fixed. -
- -
- Flix compiles to JVM bytecode and runs on the virtual machine. An earlier version of Flix
- had an optimization that would take the Option enum:
-
+ where the boolean expressions cond1, cond2, and cond3 are evaluated
+ from top to bottom until one of them returns true and then its associated body expression is evaluated.
+ The idea, quite simply, is to have a control-flow structure that visually resembles an ordinary pattern
+ match, but where there is no match value.
+
+ In hind-sight, the switch expression is nothing more than a glorified{' '}
+ if-then-else-if construct that does not carry its own weight. It is an expenditure on the
+ complexity and strangeness budget that offers almost no gain over using plain if-then-else-if
+ . Moreover, it is error-prone, because it lacks and explicit else branch in case none of the
+ conditions evaluate to true. We plan to remove it in future versions of Flix.
+
+ Like most contemporary languages, Flix uses + for string concatenation. While this is an
+ uncontroversial design choice, it does not make much sense since strings are not commutative, e.g.{' '}
+ "abc" + "def" is not the same as "def" + "abc". A better alternative
+ would be to use ++ as in Haskell. However, I believe an even better design choice would be to
+ forgo string concatenation and instead rely entirely on string interpolation. String interpolation is a
+ much more powerful and elegant solution to the problem of building complex strings.
+
The following design flaws have been fixed.
+ +
+ Flix compiles to JVM bytecode and runs on the virtual machine. An earlier version of Flix had an
+ optimization that would take the Option enum:
+
- and compile the None value to null and Some(a) to
- the underlying value of a. The idea was to save allocation and de-allocation
- of Some values, speeding up evaluation.
-
- But, this screws up interoperability with Java libraries. In Java null might
- be given a special meaning that is incompatible with the meaning None. For
- example, certain Java collections cannot contain null and trying to
- put None into one of these would raise an unexpected exception. Consequently,
- Flix no longer has this optimization.
-
- Flix aims to have a robust standard library that avoids some of the pitfalls of other
- standard libraries. We have been particularly focused on two aspects: (i) ensuring that
- functions and types have consistent names, e.g. map is
- named map for both Option and List, and (ii) to
- avoid partial functions, such as List.head and List.tail which are
- not defined for empty lists.
-
- Yet, despite these principles, we still managed to implement some problematic functions in
- the library. For example, we used to have the
- functions Option.isNone and Options.isSome. The problem with these
- functions is that they are not really useful and they lead to brittle code. For
- example, if Options.isSome returns true then that
- information cannot be used to unwrap the option anyway. Thus such functions are not
- really useful.
-
- Inspired by Scala, early versions of Flix did not always use parentheses to mark a - function call. For example, the function: -
- -- could be called by writing: -
- -
- The problem with this design is at least two-fold: (i) it hides when a function is applied,
- which is terrible in a language with side-effects, and (ii) how does one express the
- closure of f? (In Scala the answer is to write f _ ).
-
- Today, in Flix, the code is written as: -
- - -
+ and compile the None value to null and Some(a) to the underlying
+ value of a. The idea was to save allocation and de-allocation of Some values,
+ speeding up evaluation.
+
+ But, this screws up interoperability with Java libraries. In Java null might be given a
+ special meaning that is incompatible with the meaning None. For example, certain Java
+ collections cannot contain null and trying to put None into one of these would
+ raise an unexpected exception. Consequently, Flix no longer has this optimization.
+
+ Flix aims to have a robust standard library that avoids some of the pitfalls of other standard libraries.
+ We have been particularly focused on two aspects: (i) ensuring that functions and types have consistent
+ names, e.g. map is named map for both Option and List,
+ and (ii) to avoid partial functions, such as List.head and List.tail which are
+ not defined for empty lists.
+
+ Yet, despite these principles, we still managed to implement some problematic functions in the library.
+ For example, we used to have the functions Option.isNone and Options.isSome. The
+ problem with these functions is that they are not really useful and they lead to brittle code. For
+ example, if Options.isSome returns true then that information cannot be
+ used to unwrap the option anyway. Thus such functions are not really useful.
+
+ Inspired by Scala, early versions of Flix did not always use parentheses to mark a function call. For + example, the function: +
+ +could be called by writing:
+ +
+ The problem with this design is at least two-fold: (i) it hides when a function is applied, which is
+ terrible in a language with side-effects, and (ii) how does one express the closure of f? (In
+ Scala the answer is to write f _ ).
+
Today, in Flix, the code is written as:
+ +- which makes it clear when there is a function call. -
- -
- In Flix, a function f can be called with the
- arguments x and y in three ways: In standard prefix-style f(x,
- y), in infix-style x `f` y, and in postfix-style x.f(y).
- The latter is also sometimes referred to as universal function call syntax. I personally
- feel reasonably confident that all three styles are worth supporting. The postfix-style fits
- well for function calls such as a.length() where
- the length function feels closely associated with the receiver argument. The
- infix-style fits well with user-defined binary operations such as x `lub`
- y where lub is the least upper bound
- of x and y. And of course the prefix-style is the standard way
- to perform a function call.
-
- Type constructors, such as Option and Result can be thought of
- a special type of functions. Hence, it makes sense that their syntax should mirror function
- applications. For example, we can write the type
- applications Option[Int32] and Result[Int32,
- Int32] mirroring the prefix style of regular function applications. Similarly, for a
- while, Flix supported infix and postfix type applications. That is, the former could
- also be expressed as: Int32.Option[] and Int32.Result[Int32], or even
- as Int32 `Result` Int32. Thankfully, those days are gone. Striving for such
- uniformity in every place does not seem worth it.
-
- The Flix compiler comes with more than 6,500 manually written unit tests. Each unit test is - a Flix function that performs some computation, often with an expected result. The unit - tests are expressed in Flix itself. For example: -
- -which makes it clear when there is a function call.
+ +
+ In Flix, a function f can be called with the arguments x and y in
+ three ways: In standard prefix-style f(x, y), in infix-style x `f` y, and in
+ postfix-style x.f(y). The latter is also sometimes referred to as universal function call
+ syntax. I personally feel reasonably confident that all three styles are worth supporting. The
+ postfix-style fits well for function calls such as a.length() where the length{' '}
+ function feels closely associated with the receiver argument. The infix-style fits well with user-defined
+ binary operations such as x `lub` y where lub is the least upper bound of{' '}
+ x and y. And of course the prefix-style is the standard way to perform a
+ function call.
+
+ Type constructors, such as Option and Result can be thought of a special type of
+ functions. Hence, it makes sense that their syntax should mirror function applications. For example, we
+ can write the type applications Option[Int32] and Result[Int32, Int32] mirroring
+ the prefix style of regular function applications. Similarly, for a while, Flix supported infix and
+ postfix type applications. That is, the former could also be expressed as:{' '}
+ Int32.Option[] and Int32.Result[Int32], or even as{' '}
+ Int32 `Result` Int32. Thankfully, those days are gone. Striving for such uniformity in every
+ place does not seem worth it.
+
+ The Flix compiler comes with more than 6,500 manually written unit tests. Each unit test is a Flix + function that performs some computation, often with an expected result. The unit tests are expressed in + Flix itself. For example: +
+ +- In earlier versions of Flix such unit tests were expressed by manually constructing "small" - abstract syntax tree fragments. For example, the above test would be expressed as something - like: -
++ In earlier versions of Flix such unit tests were expressed by manually constructing "small" abstract + syntax tree fragments. For example, the above test would be expressed as something like: +
-- The problem with such tests is at least two-fold: (i) the tests turn out to be anything - but small and (ii) maintenance becomes an absolute nightmare. I found that the surface - syntax of Flix has remained relatively stable over time, but the abstract syntax trees - have changed frequently, making maintenance of such test cases tedious and time - consuming. -
++ The problem with such tests is at least two-fold: (i) the tests turn out to be anything but small and (ii) + maintenance becomes an absolute nightmare. I found that the surface syntax of Flix has remained relatively + stable over time, but the abstract syntax trees have changed frequently, making maintenance of such test + cases tedious and time consuming. +
-- These ideas were fortunately never implemented in Flix. -
+These ideas were fortunately never implemented in Flix.
-- The idea was to introduce a special keyword that within a pattern match would refer to - the match value. For example: -
++ The idea was to introduce a special keyword that within a pattern match would refer to the match value. + For example: +
-
- The keyword itself refers to the value of the match expression, i.e. the
- value of e. The idea was that in very large and complicated pattern matches,
- with many local variables, the itself keyword could always be used to refer to
- the innermost match value. The thinking was that this would make it easier to avoid mistakes
- such as returning e0 instead of e or the like.
-
- The problem with this idea is at least three-fold: (i) it seems like overkill for a very - specific problem, (ii) it is not worth it on the complexity and strangeness - budget, and finally (iii) it is still brittle in the presence of nested pattern matches. -
- -- It is debatable whether the following feature is a design flaw or not. -
- -- Flix has a principle that states that the standard library should not be "blessed". - That is, the standard library should be independent of the Flix compiler and language. - It should just be like any other library: A collection of Flix code. -
- -- Yet, despite this principle, Flix has special syntax for Lists, Sets and Maps: -
- -
+ The keyword itself refers to the value of the match expression, i.e. the value of{' '}
+ e. The idea was that in very large and complicated pattern matches, with many local
+ variables, the itself keyword could always be used to refer to the innermost match value. The
+ thinking was that this would make it easier to avoid mistakes such as returning e0 instead of{' '}
+ e or the like.
+
+ The problem with this idea is at least three-fold: (i) it seems like overkill for a very specific problem, + (ii) it is not worth it on the complexity and strangeness budget, and finally (iii) it is still brittle in + the presence of nested pattern matches. +
+ +It is debatable whether the following feature is a design flaw or not.
+ ++ Flix has a principle that states that the standard library should not be "blessed". That is, the standard + library should be independent of the Flix compiler and language. It should just be like any other library: + A collection of Flix code. +
+ +Yet, despite this principle, Flix has special syntax for Lists, Sets and Maps:
+ +
- which is built-in to the language. While technically these constructs are merely
- syntactic sugar for Cons, and calls
- to Set.empty, Set.insert, Map.empty and Map.insert there
- is no getting around the fact that this is a special kind of blessing of the standard
- library. In particular, it is not possible to define your
- own Foo#... syntax for anything.
-
+ which is built-in to the language. While technically these constructs are merely syntactic sugar for{' '}
+ Cons, and calls to Set.empty, Set.insert, Map.empty{' '}
+ and Map.insert there is no getting around the fact that this is a special kind of blessing of
+ the standard library. In particular, it is not possible to define your own Foo#...{' '}
+ syntax for anything.
+
- Posted April 2020 by Magnus Madsen. -
- -- It has been said that there are only two hard problems in computer science: (i) naming, (ii) - cache invalidation, and (iii) off-by-one errors. In this blog post, I will explain a name - consistency issue that arises when a programming language wants to support both - functional and destructive operations. (A functional operation always returns new data, - whereas a destructive operation mutates existing data. For example, functionally reversing - an array returns a new array with its elements reversed, whereas destructively - reversing an array mutates the array in place.) -
- -- Flix supports functional, imperative, and logic programming. Flix is intended to - be functional-first which simply means that if there is a trade-off between - having better functional- or imperative programming support, we tend to favor design choices - that support functional programming. For example, the Flix effect system separates pure - and impure functions mostly to the benefit of functional programming. -
- -- Flix, being imperative, wants to support mutable data structures such as arrays, mutable - sets and maps. We have recently added support for all three. But let us for a moment - consider a simpler data structure: the humble list. -
- -
- We can map a function f: a -{">"} b over a list l to
- obtain a new list of type List[b]:
-
- (Here the ef denotes that the function is effect polymorphic, but that
- is for another day.)
-
- We can also map a function over an option:
-
- We can also map a function over an array:
-
- This is good news: we can program with arrays in a functional-style. Mapping over an array - is certainly meaningful and useful. It might even be faster than mapping over a list! - Nevertheless, the main reason for having arrays (and mutable sets and maps) is to program - with them imperatively. We want to have operations that mutate their data. -
- -
- We want an operation that applies a function to every element of an array changing
- it in place. What should such an operation be called? We cannot name
- it map because that name is already taken by the functional version.
- Let us simply call it mapInPlace for now:
-
- The signature of mapInPlace is different from the signature
- of map in two important ways:
-
-
Unit instead of returning an array.a -{">"} a rather than a function of
- type a -{">"} b.
-
- The latter is required because the type of an array is fixed. An array of bytes cannot
- be replaced by an array of strings. Consequently, mapInPlace must take a
- less generic function of type a -{">"} a.
-
- We have seen that it is useful to have both functional and destructive functions such
- as map and mapInPlace, but what should such functions be called?
- Are they sufficiently similar that they should share similar names? What should be the
- general rule for naming functional operations and their counter-part destructive operations?
-
- To answer these questions, we surveyed the Flix standard library to understand what - names are currently being used. The table below shows a small cross section of the results: -
- --
| Functional Operation | -Destructive Equivalent | -
|---|---|
| Array.map | -Array.mapInPlace | -
| Array.reverse | -Array.reverseInPlace | -
| missing | -Array.sortByInPlace | -
| Set.insert | -not relevant – immutable | -
| Set.union | -not relevant – immutable | -
| missing | -MutSet.add | -
| missing | -MutSet.addAll | -
| MutSet.map | -MutSet.transform | -
- The table exposes the lack of any established naming convention. Let us consider some of the
- many inconsistencies: For arrays, the functional and destructive operations are
- named Array.map and Array.mapInPlace, but for mutable sets the
- operations are named MutSet.map and MutSet.transform.
- As another example, for immutable sets, we
- have Set.insert and Set.union, but these
- functional operations are missing on the mutable set. Moreover, the mutable version
- of Set.union is called Set.addAll.
- Finally, Array.sortByInPlace, what a name!
-
- With these examples in mind, we tried to come up with a principled approach to naming. Our - exploration ended up with the following options: -
- -Array.map and Array.transform,
- and MutSet.union and MutSet.addAll. We reserve the most
- common names (e.g. map) for the functional operations.
- reverse be called?
- reverseInPlace, inPlaceReverse, reverseMut,
- or similar.
- reverse!, reverse*, or the like.
- Array.reverse and MutArray.reverse.
- reverse with different semantics and (ii) we
- get a plethora of namespaces for data structures that exist in both
- immutable and mutable variants. For example, we might end up
- with Set.map (functional map on an immutable
- set), MutSet.Mut.map (destructive map on a mutable set),
- and MutSet.Imm.map (functional map on a mutable set).
- sorted operation functionally returns a new
- sorted list whereas the sort operation destructively sorts a list in place.
- We use the same scheme
- for reverse and reversed, map and mapped,
- and so forth.
- map and reverse would be reserved for destructive
- operations (unless we adopt the opposite convention of Python).
- a.toList().reverse().toArray().
- - We debated these options and slept on them for a few nights before we ultimately ended up - with the following hybrid principles: -
- -Array and MutSet support
- the map operation. Flix, being functional-first, reserves functional names
- for functional operations. Across the standard library map has the same
- name and the same type signature.
- Array.reverse(a) returns a new array with the elements
- of a in reverse order, whereas Array.reverse!(a) destructively
- re-orders the elements of a. Note: This principle applies to destructive
- operations that operate on data structures, not to impure functions in general,
- e.g. Console.printLine.
-
- As a side-note: Scheme has used ! to indicate destructive operations for a
- long-time.
-
Array.reverse and Array.reverse! share the
- same name. On the other hand, Array.transform! is
- called transform! and not map! because its type signature is
- dissimilar to map (i.e. map works on functions of type a -{">"} b, but
- transform requires functions of type a -{">"} a.)
- - We are in the process of refactoring the standard library to satisfy these new principles. -
- -- Going forward, we are sensitive to at least four potential issues: - -
- As Flix continues to mature, we will keep an eye on these issues. -
- -- Until next time, happy hacking. -
- - -+ Posted April 2020 by Magnus Madsen. +
+ ++ It has been said that there are only two hard problems in computer science: (i) naming, (ii) cache + invalidation, and (iii) off-by-one errors. In this blog post, I will explain a{' '} + name consistency issue that arises when a programming language wants to support both functional and + destructive operations. (A functional operation always returns new data, whereas a destructive operation + mutates existing data. For example, functionally reversing an array returns a new array with its + elements reversed, whereas destructively reversing an array mutates the array in place.) +
+ ++ Flix supports functional, imperative, and logic programming. Flix is intended to be{' '} + functional-first which simply means that if there is a trade-off between having better functional- + or imperative programming support, we tend to favor design choices that support functional programming. + For example, the Flix effect system separates pure and impure functions mostly to the benefit of + functional programming. +
+ ++ Flix, being imperative, wants to support mutable data structures such as arrays, mutable sets and maps. We + have recently added support for all three. But let us for a moment consider a simpler data structure: the + humble list. +
+ +
+ We can map a function f: a -{'>'} b over a list l to obtain a new
+ list of type List[b]:
+
+ (Here the ef denotes that the function is effect polymorphic, but that is for another
+ day.)
+
+ We can also map a function over an option:
+
+ We can also map a function over an array:
+
+ This is good news: we can program with arrays in a functional-style. Mapping over an array is certainly + meaningful and useful. It might even be faster than mapping over a list! Nevertheless, the main reason for + having arrays (and mutable sets and maps) is to program with them imperatively. We want to have + operations that mutate their data. +
+ +
+ We want an operation that applies a function to every element of an array changing it in place.{' '}
+ What should such an operation be called? We cannot name it map because that name is
+ already taken by the functional version. Let us simply call it mapInPlace for now:
+
+ The signature of mapInPlace is different from the signature of map in two
+ important ways:
+
Unit instead of returning an array.
+ a -{'>'} a rather than a function of type{' '}
+ a -{'>'} b.
+
+ The latter is required because the type of an array is fixed. An array of bytes cannot be replaced by an
+ array of strings. Consequently, mapInPlace must take a less generic function of type{' '}
+ a -{'>'} a.
+
+ We have seen that it is useful to have both functional and destructive functions such as map{' '}
+ and mapInPlace, but what should such functions be called? Are they sufficiently similar that
+ they should share similar names? What should be the general rule for naming functional operations and
+ their counter-part destructive operations?
+
+ To answer these questions, we surveyed the Flix standard library to understand what names are currently + being used. The table below shows a small cross section of the results: +
+ ++
| Functional Operation | +Destructive Equivalent | +
|---|---|
| Array.map | +Array.mapInPlace | +
| Array.reverse | +Array.reverseInPlace | +
| + missing + | +Array.sortByInPlace | +
| Set.insert | +not relevant – immutable | +
| Set.union | +not relevant – immutable | +
| + missing + | +MutSet.add | +
| + missing + | +MutSet.addAll | +
| MutSet.map | +MutSet.transform | +
+ The table exposes the lack of any established naming convention. Let us consider some of the many
+ inconsistencies: For arrays, the functional and destructive operations are named Array.map{' '}
+ and Array.mapInPlace, but for mutable sets the operations are named MutSet.map{' '}
+ and MutSet.transform. As another example, for immutable sets, we have Set.insert{' '}
+ and Set.union, but these functional operations are missing on the mutable set. Moreover, the
+ mutable version of Set.union is called Set.addAll. Finally,{' '}
+ Array.sortByInPlace, what a name!
+
+ With these examples in mind, we tried to come up with a principled approach to naming. Our exploration + ended up with the following options: +
+ +Array.map and Array.transform, and MutSet.union and{' '}
+ MutSet.addAll. We reserve the most common names (e.g. map) for the functional
+ operations.
+ reverse{' '}
+ be called?
+ reverseInPlace,{' '}
+ inPlaceReverse, reverseMut, or similar.
+ reverse!, reverse*, or the like.
+ Array.reverse and MutArray.reverse.
+ reverse with different semantics and (ii) we get a plethora of namespaces
+ for data structures that exist in both immutable and mutable variants. For example, we might end up with{' '}
+ Set.map (functional map on an immutable set), MutSet.Mut.map (destructive map
+ on a mutable set), and MutSet.Imm.map (functional map on a mutable set).
+ sorted operation functionally returns a new sorted list
+ whereas the sort operation destructively sorts a list in place. We use the same scheme for{' '}
+ reverse and reversed, map and mapped, and so forth.
+ map and{' '}
+ reverse would be reserved for destructive operations (unless we adopt the opposite{' '}
+ convention of Python).
+ a.toList().reverse().toArray().
+ + We debated these options and slept on them for a few nights before we ultimately ended up with the + following hybrid principles: +
+ +Array and MutSet support the map operation. Flix, being
+ functional-first, reserves functional names for functional operations. Across the standard library{' '}
+ map has the same name and the same type signature.
+ Array.reverse(a) returns a new array with the elements of a in reverse order,
+ whereas Array.reverse!(a) destructively re-orders the elements of a. Note:
+ This principle applies to destructive operations that operate on data structures, not to impure
+ functions in general, e.g. Console.printLine.
+
+ As a side-note: Scheme has used ! to indicate destructive operations for a long-time.
+
Array.reverse and Array.reverse!{' '}
+ share the same name. On the other hand, Array.transform! is called transform!{' '}
+ and not map! because its type signature is dissimilar to map (i.e. map works on functions
+ of type a -{'>'} b, but transform requires functions of type a -{'>'} a.)
+ We are in the process of refactoring the standard library to satisfy these new principles.
+ ++ Going forward, we are sensitive to at least four potential issues: +
As Flix continues to mature, we will keep an eye on these issues.
+ +Until next time, happy hacking.
+ +- Posted May 2020 by Magnus Madsen. -
- -- In the blog post Patterns of Bugs, Walter Bright, - the author of the D programming Language, writes about his - experience working at Boeing and their attitude towards failure: -
- --- -- "[...] The best people have bad days and make mistakes, so the solution is to - change the process so the mistakes cannot happen or cannot propagate." -
- -- "One simple example is an assembly that is bolted onto the frame with four bolts. The - obvious bolt pattern is a rectangle. Unfortunately, a rectangle pattern can be assembled - in two different ways, one of which is wrong. The solution is to offset one of the bolt - holes — then the assembly can only be bolted on in one orientation. The possible - mechanic's mistake is designed out of the system." -
- -- "[...] Parts can only be assembled one way, the correct - way." -
-
- (Emphasis mine). -
- -- Bright continues to explain that these ideas are equally applicable to software: We should - build software such that it can only be assembled correctly. In this blog post, I will - discuss how this idea can be applied to the design of a type and effect system. In - particular, I will show how the Flix programming language and, by extension, its standard - library ensure that pure and impure functions are not assembled incorrectly. -
- -- A major selling point of functional programming is that it supports equational reasoning. - Informally, equational reasoning means that we can reason about programs by replacing an - expression by another one, provided they're both equal. For example, we can substitute - variables with the expressions they are bound to. -
- -- For example, if we have the program fragment: -
- -+ Posted May 2020 by Magnus Madsen. +
+ ++ In the blog post Patterns of Bugs, Walter + Bright, the author of the D programming Language, writes about his + experience working at Boeing and their attitude towards failure: +
+ +++ ++ "[...] The best people have bad days and make mistakes, so the solution is to change the process so the + mistakes cannot happen or cannot propagate." +
+ ++ "One simple example is an assembly that is bolted onto the frame with four bolts. The obvious bolt + pattern is a rectangle. Unfortunately, a rectangle pattern can be assembled in two different ways, one + of which is wrong. The solution is to offset one of the bolt holes — then the assembly can only be + bolted on in one orientation. The possible mechanic's mistake is designed out of the system." +
+ ++ "[...] Parts can only be assembled one way, the correct way." +
+
(Emphasis mine).
+ ++ Bright continues to explain that these ideas are equally applicable to software: We should build software + such that it can only be assembled correctly. In this blog post, I will discuss how this idea can be + applied to the design of a type and effect system. In particular, I will show how the Flix programming + language and, by extension, its standard library ensure that pure and impure functions are not assembled + incorrectly. +
+ ++ A major selling point of functional programming is that it supports{' '} + equational reasoning. Informally, + equational reasoning means that we can reason about programs by replacing an expression by another one, + provided they're both equal. For example, we can substitute variables with the expressions they are bound + to. +
+ +For example, if we have the program fragment:
+ +
- We can substitute for x and understand this program as:
-
+ We can substitute for x and understand this program as:
+
- Unfortunately, in the presence of side-effects, such reasoning breaks down. -
+Unfortunately, in the presence of side-effects, such reasoning breaks down.
-- For example, the program fragment: -
+For example, the program fragment:
-- is not equivalent to the program: -
- -- Most contemporary functional programming languages, including Clojure, OCaml, and Scala, - forgo equational reasoning by allow arbitrary side-effects inside functions. To be clear, - it is still common to write purely functional programs in these languages and to reason - about them using equational reasoning. The major concern is that there is no language - support to guarantee when such reasoning is valid. Haskell is the only major programming - language that guarantees equational reasoning at the cost of a total and absolute ban on - side-effects. -
- -- Flix aims to walk on the middle of the road: We want to support equational reasoning with - strong guarantees while still allowing side-effects. Our solution is a type and effect - system that cleanly separates pure and impure code. The idea of using an effect system - to separate pure and impure code is old, but our implementation, which supports type - inference and polymorphism, is new. -
- -- Flix functions are pure by default. We can write a pure function: -
- -- If we want to be explicit, but non-idiomatic, we can write: -
- -
- where \ {} specifies that the inc function is pure.
-
- We can also write an impure function: -
- -
- where \ IO specifies that the sayHello function is impure.
-
- The Flix type and effect system is sound, hence if we forget the \ IO annotation
- on the sayHello function, the compiler will emit a type (or rather effect) error.
-
- The type and effect system cleanly separates pure and impure code. If an expression is pure - then it always evaluates to the same value and it cannot have side-effects. This is part - of what makes Flix functional-first: We can trust that pure functions behave like - mathematical functions. -
- -- We have already seen that printing to the screen is impure. Other sources of impurity are - mutation of memory (e.g. writing to main memory, writing to the disk, writing to the - network, etc.). Reading from mutable memory is also impure because there is no guarantee - that we will get the same value if we read the same location twice. -
- -- In Flix, the following operations are impure: -
- -- We can use the type and effect system to restrict the purity (or impurity) of function - arguments that are passed to higher-order functions. This is useful for at least two - reasons: (i) it prevents leaky abstractions where the caller can observe implementation - details of the callee, and (ii) it can help avoid bugs in the sense of Walter Bright's - "Parts can only be assembled one way, the correct way." -
- -- We will now look at several examples of how type signatures can control purity or impurity. -
- -
- We can enforce that the predicate f passed
- to Set.exists is pure:
-
- The signature f: a -{">"} Bool denotes a pure function
- from a to Bool. Passing an impure function
- to exists is a compile-time type error. We want to enforce
- that f is pure because the contract for exists makes no guarantees
- about how f is called. The implementation of exists may
- call f on the elements in xs in any order and any number of times.
- This requirement is beneficial because its allows freedom in the implementation
- of Set, including in the choice of the underlying data structure and in the
- implementation of its operations. For example, we can implement sets using search trees or
- with hash tables, and we can perform existential queries in parallel using
- fork-join. If f was impure such implementation details would leak and be
- observable by the client. Functions can only be assembled one way, the correct way.
-
- We can enforce that the function f passed to the
- function List.foreach is impure:
-
- The signature f: a -{">"} Unit \ IO denotes an impure function
- from b to Unit. Passing a pure function to foreach is
- a compile-time type error. Given that f is impure and f is called
- within foreach, it is itself impure. We enforce that
- the f function is impure because it is pointless to apply
- a pure function with a Unit return type to every element of a list. Functions
- can only be assembled one way, the correct way.
-
- We can enforce that event listeners are impure: -
- -+ is not equivalent to the program: +
+ ++ Most contemporary functional programming languages, including Clojure, OCaml, and Scala, forgo equational + reasoning by allow arbitrary side-effects inside functions. To be clear, it is still common to write + purely functional programs in these languages and to reason about them using equational reasoning. The + major concern is that there is no language support to guarantee when such reasoning is valid. Haskell is + the only major programming language that guarantees equational reasoning at the cost of a total and + absolute ban on side-effects. +
+ ++ Flix aims to walk on the middle of the road: We want to support equational reasoning with strong + guarantees while still allowing side-effects. Our solution is a type and effect system that cleanly + separates pure and impure code. The idea of using an effect system to separate pure and impure code is + old, but our implementation, which supports type inference and polymorphism, is new. +
+ +Flix functions are pure by default. We can write a pure function:
+ +If we want to be explicit, but non-idiomatic, we can write:
+ +
+ where \ {} specifies that the inc function is pure.
+
We can also write an impure function:
+ +
+ where \ IO specifies that the sayHello function is impure.
+
+ The Flix type and effect system is sound, hence if we forget the \ IO annotation on
+ the sayHello function, the compiler will emit a type (or rather effect) error.
+
+ The type and effect system cleanly separates pure and impure code. If an expression is pure then it always + evaluates to the same value and it cannot have side-effects. This is part of what makes Flix + functional-first: We can trust that pure functions behave like mathematical functions. +
+ ++ We have already seen that printing to the screen is impure. Other sources of impurity are mutation of + memory (e.g. writing to main memory, writing to the disk, writing to the network, etc.). Reading from + mutable memory is also impure because there is no guarantee that we will get the same value if we read the + same location twice. +
+ +In Flix, the following operations are impure:
+ ++ We can use the type and effect system to restrict the purity (or impurity) of function arguments that are + passed to higher-order functions. This is useful for at least two reasons: (i) it prevents leaky + abstractions where the caller can observe implementation details of the callee, and (ii) it can help avoid + bugs in the sense of Walter Bright's "Parts can only be assembled one way, the correct way." +
+ +We will now look at several examples of how type signatures can control purity or impurity.
+ +
+ We can enforce that the predicate f passed to Set.exists is pure:
+
+ The signature f: a -{'>'} Bool denotes a pure function from a to{' '}
+ Bool. Passing an impure function to exists is a compile-time type error. We want
+ to enforce that f is pure because the contract for exists makes no guarantees
+ about how f is called. The implementation of exists may call f on
+ the elements in xs in any order and any number of times. This requirement is{' '}
+ beneficial because its allows freedom in the implementation of Set, including in the
+ choice of the underlying data structure and in the implementation of its operations. For example, we can
+ implement sets using search trees or with hash tables, and we can perform existential queries in parallel
+ using fork-join. If f was impure such implementation details would leak and be observable by
+ the client. Functions can only be assembled one way, the correct way.
+
+ We can enforce that the function f passed to the function List.foreach is{' '}
+ impure:
+
+ The signature f: a -{'>'} Unit \ IO denotes an impure function from b to{' '}
+ Unit. Passing a pure function to foreach is a compile-time type error. Given
+ that f is impure and f is called within foreach, it is itself
+ impure. We enforce that the f function is impure because it is pointless to apply a{' '}
+ pure function with a Unit return type to every element of a list.{' '}
+ Functions can only be assembled one way, the correct way.
+
We can enforce that event listeners are impure:
+ +- Event listeners are always executed for their side-effect: it would be pointless to register - a pure function as an event listener. -
++ Event listeners are always executed for their side-effect: it would be pointless to register a pure + function as an event listener. +
-- We can enforce that assertion and logging facilities are given pure functions: -
+We can enforce that assertion and logging facilities are given pure functions:
-
- We want to support assertions and log statements that can be enabled and disabled at
- run-time. For efficiency, it is critical that when assertions or logging is disabled, we do
- not perform any computations that are redundant. We can achieve this by having the assert
- and log functions take callbacks that are only invoked when required. A critical property of
- these functions is that they must not influence the execution of the program. Otherwise, we
- risk situations where enabling or disabling assertions or logging may impact the presence or
- absence of a buggy execution. We can prevent such situations by requiring that the functions
- passed to assert and log are pure.
-
- We can enforce that user-defined equality functions are pure. We want purity because the - programmer should not make any assumptions about how such functions are used. Moreover, most - collections (e.g. sets and maps) require that equality does not change over time to maintain - internal data structure invariants. Similar considerations apply to hash and comparator - functions. -
- -- In the same spirit, we can enforce that one-shot comparator functions are pure: -
- -
+ We want to support assertions and log statements that can be enabled and disabled at run-time. For
+ efficiency, it is critical that when assertions or logging is disabled, we do not perform any computations
+ that are redundant. We can achieve this by having the assert and log functions take callbacks that are
+ only invoked when required. A critical property of these functions is that they must not influence the
+ execution of the program. Otherwise, we risk situations where enabling or disabling assertions or logging
+ may impact the presence or absence of a buggy execution. We can prevent such situations by requiring that
+ the functions passed to assert and log are pure.
+
+ We can enforce that user-defined equality functions are pure. We want purity because the programmer should + not make any assumptions about how such functions are used. Moreover, most collections (e.g. sets and + maps) require that equality does not change over time to maintain internal data structure invariants. + Similar considerations apply to hash and comparator functions. +
+ +In the same spirit, we can enforce that one-shot comparator functions are pure:
+ +
- We can enforce that the next function passed
- to List.unfoldWithIter is impure:
-
- The unfoldWithIter function is a variant of the unfoldWith function where each
- invocation of next changes some mutable state until the unfold completes. For
- example, unfoldWithIter is frequently used to convert Java-style iterators into
- lists. We want to enforce that next is impure because otherwise it is pointless
- to use unfoldWithIter. If next is pure then it must always either
- (i) return None which results in the empty list or (ii)
- return Some(v) for a value v which would result in an infinite
- execution.
-
- We can use purity to reject useless statement expressions. For example, the program: -
- -
+ We can enforce that the next function passed to List.unfoldWithIter is impure:
+
+ The unfoldWithIter function is a variant of the unfoldWith function where each invocation of{' '}
+ next changes some mutable state until the unfold completes. For example,{' '}
+ unfoldWithIter is frequently used to convert Java-style iterators into lists. We want to
+ enforce that next is impure because otherwise it is pointless to use{' '}
+ unfoldWithIter. If next is pure then it must always either (i) return{' '}
+ None which results in the empty list or (ii) return Some(v) for a value{' '}
+ v which would result in an infinite execution.
+
We can use purity to reject useless statement expressions. For example, the program:
+ +- is rejected with the compiler error: -
+is rejected with the compiler error:
-
- Notice that the List.map(...) expression is pure because the function x
- -> x + 1 is pure.
-
- Flix supports effect polymorphism which means that the effect of a higher-order function can - depend on the effects of its function arguments. -
- -
- For example, here is the type signature of List.map:
-
- The syntax f: a -{">"} b \ ef denotes a function
- from a to b with latent effect ef. The signature of
- the map function captures that its
- effect ef depends on the effect of its argument f.
- That is, if map is called with a pure function then its evaluation is pure,
- whereas if it is called with an impure function then its evaluation is impure. The effect
- signature is conservative (i.e. over-approximate). That is,
- the map function is considered impure even in the special case when the list is
- empty and its execution is actually pure.
-
- The type and effect system can express combinations of effects using boolean operations.
- We can, for example, express that forward function composition >> is pure
- if both its arguments are pure:
-
- Here the function f has effect ef1 and g has
- effect ef2. The returned function has effect ef1 and ef2, i.e. for it
- to be pure both ef1 and ef2 must be pure. Otherwise it is impure.
-
- Let us take a short detour. -
- -
- In a purely functional programming language, such as Haskell, mapping two
- functions f and g over a list xs is equivalent to
- mapping their composition over the list. That is:
-
- We can use such an equation to (automatically) rewrite the program to one that executes more - efficiently because the code on the right only traverses the list once and avoids - allocation of an intermediate list. Haskell already has support for such rewrite rules built into the language. -
- -- It would be desirable if we could express the same rewrite rules for programming languages - such as Clojure, OCaml, and Scala. Unfortunately, identities - such as the above - do not - hold in the presence of side-effects. For example, the program: -
- -
+ Notice that the List.map(...) expression is pure because the function{' '}
+ x -> x + 1 is pure.
+
+ Flix supports effect polymorphism which means that the effect of a higher-order function can depend on the + effects of its function arguments. +
+ +
+ For example, here is the type signature of List.map:
+
+ The syntax f: a -{'>'} b \ ef denotes a function from a to b with
+ latent effect ef. The signature of the map function captures that its effect{' '}
+ ef depends on the effect of its argument f. That is, if map is
+ called with a pure function then its evaluation is pure, whereas if it is called with an impure function
+ then its evaluation is impure. The effect signature is conservative (i.e. over-approximate). That
+ is, the map function is considered impure even in the special case when the list is empty and
+ its execution is actually pure.
+
+ The type and effect system can express combinations of effects using boolean operations. We can, for
+ example, express that forward function composition >> is pure if both its arguments are
+ pure:
+
+ Here the function f has effect ef1 and g has effect{' '}
+ ef2. The returned function has effect ef1 and ef2, i.e. for it to be pure both{' '}
+ ef1 and ef2 must be pure. Otherwise it is impure.
+
Let us take a short detour.
+ +
+ In a purely functional programming language, such as Haskell, mapping two functions f and{' '}
+ g over a list xs is equivalent to mapping their composition over the list. That
+ is:
+
+ We can use such an equation to (automatically) rewrite the program to one that executes more efficiently + because the code on the right only traverses the list once and avoids allocation of an intermediate list. + Haskell already has support for such rewrite rules{' '} + built into the language. +
+ ++ It would be desirable if we could express the same rewrite rules for programming languages such as + Clojure, OCaml, and Scala. Unfortunately, identities - such as the above - do not hold in the presence of + side-effects. For example, the program: +
+ +
- prints 1, 2, 3, 1, 2, 3. But, if we apply the rewrite rule, the transformed
- program now prints 1, 1, 2, 2, 3, 3! In the presence of side-effects we cannot
- readily apply such rewrite rules.
-
- We can use the Flix type and effect to ensure that a rewrite rule like the above is only
- applied when both f and g are pure!
-
- We can, in fact, go even further. If at most
- one of f and g is impure then it is still safe to apply
- the above rewrite rule. Furthermore, the Flix type and effect system is sufficiently
- expressive to capture such a requirement!
-
- We can distill the essence of this point into the type signature: -
- -
- It is not important exactly what mapCompose does (or even if it makes sense).
- What is important is that it has a function signature that requires two function
- arguments f and g of which at most one may be impure.
-
- To understand why, let us look closely at the signature of mapCompose:
-
-
e1 = T (i.e. f is pure) then (not e1) or e2 = F
- or e2 = e2. In other words, g may be pure or impure. Its purity
- is not constrained by the type signature.
- e1 = F (i.e. f is impure)
- then (not e1) or e2 = T or e2 = T .
- In other words, g must be pure, otherwise there is a type error.
-
- If you think about it, the above is equivalent to the requirement that at most one
- of f and g may be impure.
-
- Without going into detail, an interesting aspect of the type and effect system is
- that we might as well have given mapCompose the equivalent (equi-most general)
- type signature:
-
- where the effects of f and g are swapped.
-
- It is not uncommon for functions to be internally impure but observationally pure. - That is, a function may use mutation and perform side-effects without it being observable - by the external world. We say that such side-effects are benign. Fortunately, we can - still treat such functions as pure with an explicit effect cast. -
- -- For example, we can call a Java method (which may have arbitrary side-effects) but - explicitly mark it as pure with an effect cast: -
- -
+ prints 1, 2, 3, 1, 2, 3. But, if we apply the rewrite rule, the transformed program now
+ prints 1, 1, 2, 2, 3, 3! In the presence of side-effects we cannot readily apply such rewrite
+ rules.
+
+ We can use the Flix type and effect to ensure that a rewrite rule like the above is only applied when both{' '}
+ f and g are pure!
+
+ We can, in fact, go even further. If at most one of f and g is impure
+ then it is still safe to apply the above rewrite rule. Furthermore, the Flix type and effect system is
+ sufficiently expressive to capture such a requirement!
+
We can distill the essence of this point into the type signature:
+ +
+ It is not important exactly what mapCompose does (or even if it makes sense). What is
+ important is that it has a function signature that requires two function arguments f and{' '}
+ g of which at most one may be impure.
+
+ To understand why, let us look closely at the signature of mapCompose:
+
+
e1 = T (i.e. f is pure) then (not e1) or e2 = F or e2 = e2.
+ In other words, g may be pure or impure. Its purity is not constrained by the type
+ signature.
+ e1 = F (i.e. f is impure) then{' '}
+ (not e1) or e2 = T or e2 = T . In other words, g must be pure,
+ otherwise there is a type error.
+
+ If you think about it, the above is equivalent to the requirement that at most one of f and{' '}
+ g may be impure.
+
+ Without going into detail, an interesting aspect of the type and effect system is that we might as well
+ have given mapCompose the equivalent (equi-most general) type signature:
+
+ where the effects of f and g are swapped.
+
+ It is not uncommon for functions to be internally impure but observationally pure. That is, a function may + use mutation and perform side-effects without it being observable by the external world. We say that such + side-effects are benign. Fortunately, we can still treat such functions as pure with an explicit{' '} + effect cast. +
+ ++ For example, we can call a Java method (which may have arbitrary side-effects) but explicitly mark it as + pure with an effect cast: +
+ +
- We know that java.lang.String.charAt has is pure hence the cast is safe.
-
- An effect cast, like an ordinary cast, must be used with care. A cast is a mechanism - that allows the programmer to subvert the type (and effect) system. It is the - responsibility of the programmer to ensure that the cast is safe. Unlike type casts, an - effect cast cannot be checked at run-time with the consequence that an unsound effect cast - may silently lead to undefined behavior. -
- -- Here is an example of a pure function that is implemented internally using mutation: -
- -
+ We know that java.lang.String.charAt has is pure hence the cast is safe.
+
+ An effect cast, like an ordinary cast, must be used with care. A cast is a mechanism that allows the + programmer to subvert the type (and effect) system. It is the responsibility of the programmer to ensure + that the cast is safe. Unlike type casts, an effect cast cannot be checked at run-time with the + consequence that an unsound effect cast may silently lead to undefined behavior. +
+ +Here is an example of a pure function that is implemented internally using mutation:
+ +
- Internally, stripIndentHelper uses a mutable string builder.
-
- The Flix type and effect system supports inference. Explicit type annotations are never - required locally within a function. As a design choice, we do require type signatures for - top-level definitions. Within a function, the programmer never has to worry about pure and - impure expressions; the compiler automatically infers whether an expression is pure, impure, - or effect polymorphic. The programmer only has to ensure that the declared type and effect - matches the type and effect of the function body. -
- -- The details of the type and effect system are the subject of a forthcoming research paper - and will be made available in due time. -
- -- The Flix type and effect system separates pure and impure code. The upshot is that a - functional programmer can trust that a pure function behaves like a mathematical function: - it returns the same result when given the same arguments. At the same time, we are still - allowed to write parts of the program in an impure, imperative style. Effect polymorphism - ensures that both pure and impure code can be used with higher-order functions. -
- -
- We can also use effects to control when higher-order functions require pure (or impure)
- functions. We have seen several examples of such use cases, e.g. requiring
- that Set.count takes a pure function or
- that List.unfoldWithIter takes an impure function. Together, these restrictions
- ensure that functions can only be assembled in one way, the correct way.
-
- Until next time, happy hacking. -
- - -
+ Internally, stripIndentHelper uses a mutable string builder.
+
+ The Flix type and effect system supports inference. Explicit type annotations are never required locally + within a function. As a design choice, we do require type signatures for top-level definitions. Within a + function, the programmer never has to worry about pure and impure expressions; the compiler automatically + infers whether an expression is pure, impure, or effect polymorphic. The programmer only has to ensure + that the declared type and effect matches the type and effect of the function body. +
+ ++ The details of the type and effect system are the subject of a forthcoming research paper and will be made + available in due time. +
+ ++ The Flix type and effect system separates pure and impure code. The upshot is that a functional programmer + can trust that a pure function behaves like a mathematical function: it returns the same result when given + the same arguments. At the same time, we are still allowed to write parts of the program in an impure, + imperative style. Effect polymorphism ensures that both pure and impure code can be used with higher-order + functions. +
+ +
+ We can also use effects to control when higher-order functions require pure (or impure) functions. We have
+ seen several examples of such use cases, e.g. requiring that Set.count takes a pure function
+ or that List.unfoldWithIter takes an impure function. Together, these restrictions ensure
+ that functions can only be assembled in one way, the correct way.
+
Until next time, happy hacking.
+ + + + ) + } } export default PolymorphicEffects diff --git a/src/page/blog/ProgrammingLanguageDefense.js b/src/page/blog/ProgrammingLanguageDefense.js index abe8282..d941644 100644 --- a/src/page/blog/ProgrammingLanguageDefense.js +++ b/src/page/blog/ProgrammingLanguageDefense.js @@ -1,341 +1,320 @@ -import React, {Component} from "react"; -import {Col, Container, Row} from "reactstrap"; -import {Link} from "react-router-dom"; +import React, { Component } from 'react' +import { Col, Container, Row } from 'reactstrap' +import { Link } from 'react-router-dom' class ProgrammingLanguageDefense extends Component { - - componentDidMount() { - document.title = "Flix | In Defense of Programming Languages"; - } - - render() { - return ( -- Posted July 2021 by Magnus Madsen. Thanks to Matthew Lutze for discussion and - comments on an early draft. -
- -- This blog post is written in defense of programming language enthusiasts; whether they are - compiler hackers, programming language hobbyists, industry professionals, or academics. -
- -- In this blog post, I want to examine the discourse around programming languages and - especially how new programming languages are received. My hope is to improve communication - between programming languages designers and software developers. I understand that - we cannot all agree, but it would be fantastic if everyone could at least try to be - friendly, to be intellectually curious, and to give constructive feedback! -
- -- Let me set the stage with a few quotes from social media tech sites (e.g. Reddit, - HackerNews, Twitter, etc.). I have lightly edited and anonymized the following quotes: -
- --- -"Great! Yet-another-programming-language™. This is exactly what we - need; the gazillion of existing programming languages is not enough!"
- -
-- -"This is – by far – the worst syntax I have ever seen in a functional - language!"
- -
-- -"The language is probably great from a technical point of view, but - unless Apple, Google, Mozilla, or Microsoft is on-board it is pointless."
- -
-- -"How can anyone understand such weird syntax? I hate all these - symbols."
- -
-- -"The examples all look horrible. The site looks horrible. This needs a - lot of work before it gets close to anything I would even consider using."
- -
- While all of the above quotes are in response to news about the Flix programming language - (on whose website you are currently reading this blog post), depressingly similar comments - are frequently posted in response to news about other new programming languages. -
- -- Why do people post such comments? And what can be done about it? -
- -- I think there are two reasons which are grounded in legitimate concerns: -
- --
- Of course there are also internet trolls; but let us ignore them. -
- -- I want to give a point-by-point rebuttal to the most common refrains heard whenever a new - programming language is proposed. -
- -- The Flix FAQ joking responds to this question with a rhetorical - question: Do we really need safer airplanes? Do we really need electric cars? Do we - really need more ergonomic chairs? -
- -- I think it is a valid argument. We want better programming languages because we want to - offer software developers better tools to write their programs. You might say that existing - programming languages already have all the feature we need, but I think that there are - exciting developments; both brand new ideas and old research ideas that are making their - way into new programming languages: -
- --
- I don't think we are anywhere near to the point where programming languages are as good as - they are ever going to get. On the contrary, I think we are still in the infancy of - programming language design. -
- -- I strongly disagree. I think we are experiencing a period of programming language - fragmentation after a long period of consolidation and stagnation. For the last 15-years or - so, the industry has been dominated by C, C++, C# and Java. The market share of these - programming languages was always increasing and they were the default safe choice for new - software projects. -
- -- Today that is no longer the case. The ecosystem of programming languages is much more - diverse (and stronger for it). We have Rust. We have Scala. We also have Go, Python, and - JavaScript. There is also Crystal, Elixir, Elm, and Nim (Oh, and Flix of course!) We are in - a period of fragmentation. After a decade of object-oriented ossification we are entering a - new and exciting period! -
- -- If history repeats itself then at some point we will enter a new period of consolidation. - It is too early to speculate on which programming languages will be the winners, but I feel - confident that they will be much better than C, C++, C#, and Java! (Ok, maybe C++30 will be - one of them – that language changes as much as Haskell!) -
- -- (Addendum: That said, it is true that many hobby programming languages look the same. But - there is a reason for that: if you want to learn about compilers it makes sense to start by - implementing a minimal functional or object-oriented programming language.) -
- -- That's the way of the world. -
- -- What do you think an airline pilot from the 1950's would say if he or she entered the flight - deck of an Airbus A350? Sure, the principles of flying are the same, and indeed iteration - and recursion are not going anywhere. But we cannot expect everything to stay the same. All - those instruments are there for a reason and they make flying safer and more efficient. -
- -
- As another example, once universities start teaching Rust (and we will!) then programming
- with ownership and lifetimes will become commonplace. As yet another example, today every
- programmer can reasonably be expected to know about filter and map,
- but that was certainly not the case 15 years ago!
-
- Historically that has not been true. Neither PHP, Python, Ruby, Rust, or Scala had - major tech companies behind them. If industry support came, it came at a later time. -
- -- With these points in mind, I want to suggest some ways to improve communication between - aspiring programming language designers and software developers: -
- -- When presenting a new programming language (or ideas related to a new language): -
- --
- The time has come to nail our colors to the flag: -
- --
- Until next time, happy hacking. -
- - -+ Posted July 2021 by Magnus Madsen. Thanks to Matthew Lutze for discussion and comments on an early + draft. +
+ ++ This blog post is written in defense of programming language enthusiasts; whether they are compiler + hackers, programming language hobbyists, industry professionals, or academics. +
+ ++ In this blog post, I want to examine the discourse around programming languages and especially how new + programming languages are received. My hope is to improve communication between programming languages + designers and software developers. I understand that we cannot all agree, but it would be fantastic if + everyone could at least try to be friendly, to be intellectually curious, and to give constructive + feedback! +
+ ++ Let me set the stage with a few quotes from social media tech sites (e.g. Reddit, HackerNews, Twitter, + etc.). I have lightly edited and anonymized the following quotes: +
+ +++ ++ "Great! Yet-another-programming-language™. This is exactly what we need; the gazillion of existing + programming languages is not enough!" +
+ +
++ +"This is – by far – the worst syntax I have ever seen in a functional language!"
+ +
++ ++ "The language is probably great from a technical point of view, but unless Apple, Google, Mozilla, or + Microsoft is on-board it is pointless." +
+ +
++ +"How can anyone understand such weird syntax? I hate all these symbols."
+ +
++ ++ "The examples all look horrible. The site looks horrible. This needs a lot of work before it gets close + to anything I would even consider using." +
+ +
+ While all of the above quotes are in response to news about the Flix programming language (on whose + website you are currently reading this blog post), depressingly similar comments are frequently posted in + response to news about other new programming languages. +
+ +Why do people post such comments? And what can be done about it?
+ +I think there are two reasons which are grounded in legitimate concerns:
+ ++
Of course there are also internet trolls; but let us ignore them.
+ ++ I want to give a point-by-point rebuttal to the most common refrains heard whenever a new programming + language is proposed. +
+ ++ The Flix FAQ joking responds to this question with a rhetorical question:{' '} + + Do we really need safer airplanes? Do we really need electric cars? Do we really need more ergonomic + chairs? + +
+ ++ I think it is a valid argument. We want better programming languages because we want to offer software + developers better tools to write their programs. You might say that existing programming languages already + have all the feature we need, but I think that there are exciting developments; both brand new ideas and + old research ideas that are making their way into new programming languages: +
+ ++
+ I don't think we are anywhere near to the point where programming languages are as good as they are ever + going to get. On the contrary, I think we are still in the infancy of programming language design. +
+ ++ I strongly disagree. I think we are experiencing a period of programming language fragmentation after a + long period of consolidation and stagnation. For the last 15-years or so, the industry has been dominated + by C, C++, C# and Java. The market share of these programming languages was always increasing and they + were the default safe choice for new software projects. +
+ ++ Today that is no longer the case. The ecosystem of programming languages is much more diverse (and + stronger for it). We have Rust. We have Scala. We also have Go, Python, and JavaScript. There is also + Crystal, Elixir, Elm, and Nim (Oh, and Flix of course!) We are in a period of fragmentation. After a + decade of object-oriented ossification we are entering a new and exciting period! +
+ ++ If history repeats itself then at some point we will enter a new period of consolidation. It is too early + to speculate on which programming languages will be the winners, but I feel confident that they will be + much better than C, C++, C#, and Java! (Ok, maybe C++30 will be one of them – that language changes + as much as Haskell!) +
+ ++ (Addendum: That said, it is true that many hobby programming languages look the same. But there is a + reason for that: if you want to learn about compilers it makes sense to start by implementing a minimal + functional or object-oriented programming language.) +
+ +That's the way of the world.
+ ++ What do you think an airline pilot from the 1950's would say if he or she entered the flight deck of an + Airbus A350? Sure, the principles of flying are the same, and indeed iteration and recursion are not going + anywhere. But we cannot expect everything to stay the same. All those instruments are there for a reason + and they make flying safer and more efficient. +
+ +
+ As another example, once universities start teaching Rust (and we will!) then programming with ownership
+ and lifetimes will become commonplace. As yet another example, today every programmer can reasonably be
+ expected to know about filter and map, but that was certainly not the case 15
+ years ago!
+
+ Historically that has not been true. Neither PHP, Python, Ruby, Rust, or Scala had major tech companies + behind them. If industry support came, it came at a later time. +
+ ++ With these points in mind, I want to suggest some ways to improve communication between aspiring + programming language designers and software developers: +
+ +When presenting a new programming language (or ideas related to a new language):
+ ++
The time has come to nail our colors to the flag:
+ ++
Until next time, happy hacking.
+ +- Posted February 2020 by Magnus Madsen. -
- -- As software developers, we strive to write correct and maintainable code. - Today, I want to share some code where I failed in these two goals. -
- -- I will show you real-world code from the Flix compiler and ask you to determine what is - wrong with the code. Then, later, I will argue how programming languages can help avoid the - type of problems you will see. (Note to the reader: The Flix compiler is (currently) written - in Scala, so the code is in Scala, but the lessons learned are applied to the Flix - programming language. I hope that makes sense.) -
- -- Let us begin our journey by looking at the following code fragment: -
- -+ Posted February 2020 by Magnus Madsen. +
+ ++ As software developers, we strive to write correct and maintainable code. Today, I want to share some code + where I failed in these two goals. +
+ ++ I will show you real-world code from the Flix compiler and ask you to determine what is wrong with the + code. Then, later, I will argue how programming languages can help avoid the type of problems you will + see. (Note to the reader: The Flix compiler is (currently) written in Scala, so the code is in Scala, but + the lessons learned are applied to the Flix programming language. I hope that makes sense.) +
+ +Let us begin our journey by looking at the following code fragment:
+ +- Do you see any issues? -
- -- If not, look again. -
- -- Ok, got it? -
- -
- The code has a subtle bug: In the case for Unary the local
- variable e holds the result of the recursion on exp. But by
- mistake the reconstruction of Unary uses exp and
- not e as intended. The local variable e is unused. Consequently,
- the specific transformations applied by visitExp under unary expressions are
- silently discarded. This bug was in the Flix compiler for some time before it was
- discovered.
-
- Let us continue our journey with the following code fragment: -
- -Do you see any issues?
+ +If not, look again.
+ +Ok, got it?
+ +
+ The code has a subtle bug: In the case for Unary the local variable e holds the
+ result of the recursion on exp. But by mistake the reconstruction of Unary uses{' '}
+ exp and not e as intended. The local variable e is unused.
+ Consequently, the specific transformations applied by visitExp under unary expressions are
+ silently discarded. This bug was in the Flix compiler for some time before it was discovered.
+
Let us continue our journey with the following code fragment:
+ +- Do you see any issues? -
+Do you see any issues?
-- If not, look again. -
+If not, look again.
-- Ok, got it? -
+Ok, got it?
-
- The code has a similar bug: The local variable eff3 is not used, but it
- should have been used to compute resultEff. While this bug never made it into
- any release of Flix, it did cause a lot of head-scratching.
-
+ The code has a similar bug: The local variable eff3 is not used, but it should have been used
+ to compute resultEff. While this bug never made it into any release of Flix, it did cause a
+ lot of head-scratching.
+
- Now we are getting the hang of things! What about this code fragment?: -
+Now we are getting the hang of things! What about this code fragment?:
-- Do you see any issues? -
- -- I am sure you did. -
- -
- The bug is the following: The formal parameter to mkOr is
- misspelled ef1f instead of eff1. But how does this even compile,
- you ask? Well, unfortunately the mkOr function is nested inside another
- function that just so happens to have an argument also named eff1!
- Damn Murphy and his laws. The intention was for the formal parameters
- of mkOr to shadow eff1 (and eff2), but because of the
- misspelling, ef1f ended up as unused and eff1 (a completely
- unrelated variable) was used instead. The issue was found during development, but not
- before several hours of wasted work. Not that I am bitter or anything...
-
- We are almost at the end of our journey! But what about this beast: -
- -Do you see any issues?
+ +I am sure you did.
+ +
+ The bug is the following: The formal parameter to mkOr is misspelled ef1f{' '}
+ instead of eff1. But how does this even compile, you ask? Well, unfortunately the{' '}
+ mkOr function is nested inside another function that just so happens to have an argument also
+ named eff1! Damn Murphy and his laws. The intention was for the formal parameters of{' '}
+ mkOr to shadow eff1 (and eff2), but because of the misspelling,{' '}
+ ef1f ended up as unused and eff1 (a completely unrelated variable) was used
+ instead. The issue was found during development, but not before several hours of wasted work. Not that I
+ am bitter or anything...
+
We are almost at the end of our journey! But what about this beast:
+ +- Do you see any issues? -
- -- If not, look again. -
- -- Ok, got it? -
- -- Still nothing? -
- -- Pause for dramatic effect. -
- -- Morpheus: What if I told you... -
- -- Morpheus: ... that the function has been maintained over a long period of time... -
- -- Morpheus: But that there is no place where the function is called! -
- -- I am sorry if that was unfair. But was it really? The Flix code base is more than 100,000 - lines of code, so it is hard to imagine that a single person can hold it in his or her head. -
- -- As these examples demonstrate, and as has been demonstrated in the research literature (see - e.g. Xie and Engler 2002), - redundant or unused code is often buggy code. -
- -- To overcome such issues, Flix is very strict about redundant and unused code. -
- -- The Flix compiler emits a compile-time error for the following redundancies: -
- --
| Type | -Description | -
|---|---|
| Unused Def | -A function is declared, but never used. | -
| Unused Enum | -An enum type is declared, but never used. | -
| Unused Enum Case | -A case (variant) of an enum is declared, but never used. | -
| Unused Formal Parameter | -A formal parameter is declared, but never used. | -
| Unused Type Parameter | -A function or enum declares a type parameter, but it is never used. | -
| Unused Local Variable | -A function declares a local variable, but it is never used. | -
| Shadowed Local Variable | -A local variable hides another local variable. | -
| Unconditional Recursion | -A function unconditionally recurses on all control-flow paths. | -
| Useless Expression Statement | -An expression statement discards the result of a pure expression. | -
- As the Flix language grows, we will continue to expand the list. -
- -- Let us look at three concrete examples of such compile-time errors. -
- -- Given the program fragment: -
- -Do you see any issues?
+ +If not, look again.
+ +Ok, got it?
+ +Still nothing?
+ ++ Pause for dramatic effect. +
+ +Morpheus: What if I told you...
+ +Morpheus: ... that the function has been maintained over a long period of time...
+ ++ Morpheus: But that there is no place where the function is called! +
+ ++ I am sorry if that was unfair. But was it really? The Flix code base is more than 100,000 lines of code, + so it is hard to imagine that a single person can hold it in his or her head. +
+ ++ As these examples demonstrate, and as has been demonstrated in the research literature (see e.g.{' '} + Xie and Engler 2002), redundant or unused code + is often buggy code. +
+ +To overcome such issues, Flix is very strict about redundant and unused code.
+ ++ The Flix compiler emits a compile-time error for the following redundancies: +
+ ++
| Type | +Description | +
|---|---|
| Unused Def | +A function is declared, but never used. | +
| Unused Enum | +An enum type is declared, but never used. | +
| Unused Enum Case | +A case (variant) of an enum is declared, but never used. | +
| Unused Formal Parameter | +A formal parameter is declared, but never used. | +
| Unused Type Parameter | +A function or enum declares a type parameter, but it is never used. | +
| Unused Local Variable | +A function declares a local variable, but it is never used. | +
| Shadowed Local Variable | +A local variable hides another local variable. | +
| Unconditional Recursion | +A function unconditionally recurses on all control-flow paths. | +
| Useless Expression Statement | +An expression statement discards the result of a pure expression. | +
As the Flix language grows, we will continue to expand the list.
+ +Let us look at three concrete examples of such compile-time errors.
+ +Given the program fragment:
+ +- The Flix compiler emits the compile-time error: -
+The Flix compiler emits the compile-time error:
- -- The error message offers suggestions for how to fix the problem or alternatively how to make - the compiler shut up (by explicitly marking the variable as unused). -
++ The error message offers suggestions for how to fix the problem or alternatively how to make the compiler + shut up (by explicitly marking the variable as unused). +
-- Modern programming languages like Elm and Rust offer a similar feature. -
+Modern programming languages like Elm and Rust offer a similar feature.
-- Given the enum declaration: -
+Given the enum declaration:
-
- If only Red and Green are used then we get the Flix compile-time
- error:
-
+ If only Red and Green are used then we get the Flix compile-time error:
+
- Again, programming languages like Elm and Rust offer a similar feature. -
+Again, programming languages like Elm and Rust offer a similar feature.
-- Given the program fragment: -
+Given the program fragment:
-- The Flix compiler emits the compile-time error: -
+The Flix compiler emits the compile-time error:
-
- The problem with the code is that the evaluation of List.map(x -{">"} x + 1, 1 :: 2 ::
- Nil) has no side-effect(s) and its result is discarded.
-
- Another classic instance of this problem is when someone calls
- e.g. checkPermission(...) and expects it to throw an exception if the user has
- insufficient permissions, but in fact, the function simply returns a boolean which is then
- discarded.
-
- But this is not your Grandma's average compile-time error. At the time of writing, I
- know of no other programming language that offers a similar warning or error with
- the same precision as Flix. If you do, please drop me a line on Gitter. (Before someone
- rushes to suggest must_use and friends, please consider whether they work in
- the presence of polymorphism as outlined below).
-
- The key challenge is to (automatically) determine whether an expression is pure
- (side-effect free) in the presence of polymorphism. Specifically, the call
- to List.map is pure because the function argument x -{">"} x +
- 1 is pure. In other words, the purity of List.map depends on the purity
- of its argument: it is effect polymorphic. The combination of type inference,
- fine-grained effect inference, and effect polymorphism is a strong cocktail that I plan to
- cover in a future blog post.
-
- Note: The above is fully implemented in master, but has not yet been "released". -
- -- I hope that I have convinced you that unused code is a threat to correct and maintainable - code. However, it is a threat that can be neutralized by better programming language design - and with minor changes to development practices. Moreover, I believe that a compiler that - reports redundant or unused code can help programmers – whether inexperienced or - seasoned – avoid stupid mistakes that waste time during development. -
- -- A reasonable concern is whether working with a compiler that rejects programs with unused - code is too cumbersome or annoying. In my experience, the answer is no. After - a small learning period, whenever you want to introduce a new code fragment that will not - immediately be used, you simple remember to prefix it with an underscore, and then later you - come back and remove the underscore when you are ready to use it. -
- -- While there might be a short adjustment period, the upside is huge: The compiler - provides an iron-clad guarantee that all my code is used. Moreover, whenever I refactor some - code, I am immediately informed if some code fragment becomes unused. I think such long-term - maintainability concerns are significantly more important than a little bit of extra work - during initial development. -
- -- Until next time, happy hacking. -
- - -
+ The problem with the code is that the evaluation of List.map(x -{'>'} x + 1, 1 :: 2 :: Nil){' '}
+ has no side-effect(s) and its result is discarded.
+
+ Another classic instance of this problem is when someone calls e.g. checkPermission(...) and
+ expects it to throw an exception if the user has insufficient permissions, but in fact, the function
+ simply returns a boolean which is then discarded.
+
+ But this is not your Grandma's average compile-time error. At the time of writing, I know of no
+ other programming language that offers a similar warning or error with the same precision as Flix. If you
+ do, please drop me a line on Gitter. (Before someone rushes to suggest must_use and friends,
+ please consider whether they work in the presence of polymorphism as outlined below).
+
+ The key challenge is to (automatically) determine whether an expression is pure (side-effect free) in the
+ presence of polymorphism. Specifically, the call to List.map is pure because the{' '}
+ function argument x -{'>'} x + 1 is pure. In other words, the purity of{' '}
+ List.map depends on the purity of its argument: it is effect polymorphic. The
+ combination of type inference, fine-grained effect inference, and effect polymorphism is a strong cocktail
+ that I plan to cover in a future blog post.
+
Note: The above is fully implemented in master, but has not yet been "released".
+ ++ I hope that I have convinced you that unused code is a threat to correct and maintainable code. However, + it is a threat that can be neutralized by better programming language design and with minor changes to + development practices. Moreover, I believe that a compiler that reports redundant or unused code can help + programmers – whether inexperienced or seasoned – avoid stupid mistakes that waste time during + development. +
+ ++ A reasonable concern is whether working with a compiler that rejects programs with unused code is too + cumbersome or annoying. In my experience, the answer is no. After a small learning period, whenever you + want to introduce a new code fragment that will not immediately be used, you simple remember to prefix it + with an underscore, and then later you come back and remove the underscore when you are ready to use it. +
+ ++ While there might be a short adjustment period, the upside is huge: The compiler provides an + iron-clad guarantee that all my code is used. Moreover, whenever I refactor some code, I am immediately + informed if some code fragment becomes unused. I think such long-term maintainability concerns are + significantly more important than a little bit of extra work during initial development. +
+ +Until next time, happy hacking.
+ + + + ) + } } export default Redundancies diff --git a/src/page/misc/Checklist.js b/src/page/misc/Checklist.js index f8a0532..078fdfc 100644 --- a/src/page/misc/Checklist.js +++ b/src/page/misc/Checklist.js @@ -1,24 +1,24 @@ -import React, {Component} from 'react'; -import {Container} from "reactstrap"; +import React, { Component } from 'react' +import { Container } from 'reactstrap' class Checklist extends Component { + componentDidMount() { + document.title = 'Flix | Programming Language Checklist' + } - componentDidMount() { - document.title = "Flix | Programming Language Checklist"; - } + render() { + return ( ++ For completeness (and fun), here is the{' '} + programming language check list for Flix: +
-- For completeness (and fun), here is the programming - language check list for Flix: -
- -
- {`You appear to be advocating a new:
+
+
+ {`You appear to be advocating a new:
[x] functional [x] imperative [ ] object-oriented [ ] procedural [ ] stack-based
[x] "multi-paradigm" [x] lazy [x] eager [x] statically-typed [ ] dynamically-typed
[x] pure [x] impure [ ] non-hygienic [ ] visual [ ] beginner-friendly
@@ -119,11 +119,11 @@ In conclusion, this is what I think of you:
[ ] This is a bad language, and you should feel bad for inventing it.
[ ] Programming in this language is an adequate punishment for inventing it.
`}
-
-
- {this.state.output.result}
- {this.state.output.result}
- {this.state.output.result}
+ {this.state.output.result}
+