General recursion in programs (that makes termination undecidable) requires a fix-point operator of type (a -> a) -> a The logical equivalent of this is an axiom (P -> P) -> P which lets you prove anything. So…
How is sequencing described in the type of join?
I think SSA is related to CPS, but I'm not sure of the correspondence with Linearity. I think the key difference (but I'm not sure), is that SSA only asserts that a variable is assigned once, but might be consumed…
I think you could say that. Another way to look at it would be to say it's about organising your code in such a way that side-effects don't really matter. For instance, if only I have access to a reference, then I'm…
I also get the impression that some people view using dynamically typed languages as a badge of honor, taking more expertise to harness the greater 'expressive' power, all whilst juggling the types in your head. Bad…
It's already been flirted with in JS I believe [1], though not specifically for Flow. The problem is that it falls down in the higher order case, which happens quite alot in JS. Also, I don't think JS has a mechanism…
I'd consider those languages optionally typed, rather than gradually typed, as they don't insert run-time type checks. Regardless, I still think it's all interesting and valuable work.
By OCaml's let syntax do you mean this: https://blog.janestreet.com/let-syntax-and-why-you-should-us...? You can also add F# computation expressions to the list!
I think the jump from 'Category' to 'Value: Anything that can be assigned to a variable.' was a somewhat jarring change in abstraction level. Also, trying to explain Monad, Comonad, or Applicative as 'jargon' is…
I'm not really sure why you need the requirement of infinite sequences to do functional programming, or the restriction of no intermediate variables. Let bindings seem like a nice thing to have.
I've done some work on dynamic type checking for JavaScript and the tricky part is always when things start going higher order; sadly this is often omitted from examples. The motivation for dynamic checking was often…
As far as I can tell this isn't dynamic, it just builds an AST. Am I missing something?
You could easily use unit tests to get better coverage.
Really interesting stuff! I tried out some higher-order examples: INPUT >>> function add(f, b) { return f(b); }; let a = add(function(x) {return x + 1}, 3); OUTPUT >>> function add(f: function, b: number): number {…
> Think about being able to specify protocols in the type system and ensuring that your client and server meet the specifications. The example in that link is about user authentication. Imagine having a proof that the…
This seems like a very simple concept when compared with other systems using software transplants [1]. The most important thing I gleaned from this is the benefit of having 'type information' (clojure specs) available…
"So, is JavaScript a truly functional programming language? The short answer is no. Without support for tail-call optimization, pattern matching, immutable data struc- tures, and other fundamental elements of functional…
This is all true, but is it not a problem that most static languages don't let you (easily) specify the kind of invariants people include in unit-tests.
The problem doesn't really have anything to do with immutability; the problem is dependency and composition. E.g. f :: A -> B g :: B -> C will let me write g(f(x)), but not f(g(x)). It does not matter if f and g are…
For those interested in the learning more about single language web applications the Links project (http://groups.inf.ed.ac.uk/links/) has been going for some time with quite a few research publications.
General recursion in programs (that makes termination undecidable) requires a fix-point operator of type (a -> a) -> a The logical equivalent of this is an axiom (P -> P) -> P which lets you prove anything. So…
How is sequencing described in the type of join?
I think SSA is related to CPS, but I'm not sure of the correspondence with Linearity. I think the key difference (but I'm not sure), is that SSA only asserts that a variable is assigned once, but might be consumed…
I think you could say that. Another way to look at it would be to say it's about organising your code in such a way that side-effects don't really matter. For instance, if only I have access to a reference, then I'm…
I also get the impression that some people view using dynamically typed languages as a badge of honor, taking more expertise to harness the greater 'expressive' power, all whilst juggling the types in your head. Bad…
It's already been flirted with in JS I believe [1], though not specifically for Flow. The problem is that it falls down in the higher order case, which happens quite alot in JS. Also, I don't think JS has a mechanism…
I'd consider those languages optionally typed, rather than gradually typed, as they don't insert run-time type checks. Regardless, I still think it's all interesting and valuable work.
By OCaml's let syntax do you mean this: https://blog.janestreet.com/let-syntax-and-why-you-should-us...? You can also add F# computation expressions to the list!
I think the jump from 'Category' to 'Value: Anything that can be assigned to a variable.' was a somewhat jarring change in abstraction level. Also, trying to explain Monad, Comonad, or Applicative as 'jargon' is…
I'm not really sure why you need the requirement of infinite sequences to do functional programming, or the restriction of no intermediate variables. Let bindings seem like a nice thing to have.
I've done some work on dynamic type checking for JavaScript and the tricky part is always when things start going higher order; sadly this is often omitted from examples. The motivation for dynamic checking was often…
As far as I can tell this isn't dynamic, it just builds an AST. Am I missing something?
You could easily use unit tests to get better coverage.
Really interesting stuff! I tried out some higher-order examples: INPUT >>> function add(f, b) { return f(b); }; let a = add(function(x) {return x + 1}, 3); OUTPUT >>> function add(f: function, b: number): number {…
> Think about being able to specify protocols in the type system and ensuring that your client and server meet the specifications. The example in that link is about user authentication. Imagine having a proof that the…
This seems like a very simple concept when compared with other systems using software transplants [1]. The most important thing I gleaned from this is the benefit of having 'type information' (clojure specs) available…
"So, is JavaScript a truly functional programming language? The short answer is no. Without support for tail-call optimization, pattern matching, immutable data struc- tures, and other fundamental elements of functional…
This is all true, but is it not a problem that most static languages don't let you (easily) specify the kind of invariants people include in unit-tests.
The problem doesn't really have anything to do with immutability; the problem is dependency and composition. E.g. f :: A -> B g :: B -> C will let me write g(f(x)), but not f(g(x)). It does not matter if f and g are…
For those interested in the learning more about single language web applications the Links project (http://groups.inf.ed.ac.uk/links/) has been going for some time with quite a few research publications.