I find it interesting that the discussion on Dependent Types lists Idris and Coq as languages and discusses Formal Verification but mostly focuses on Idris and Scala with Shapeless... but to my knowledge, Coq has actually won out in 2019 for this, and Coq has even branded itself for this specifically[0].
It's not strictly a programming language, but Scribble (a Racket language) is really the first document creation language that neither feels like a markup language with a programming language API nor a programming language with a document creation API. With this sort of setup, it is really easy to introduce arbitrary new constructs to avoid duplication or to better structure your document.
LaTex is the only system I know that comes close to this, but the language is pretty horrible to actually try and use (to be fair, LaTex has quite a bit of legacy it has to maintain).
Prolog is declarative, but it's very different to SQL and it's a shame to put the two together. It is much more interesting to examine Prolog from the logic programming point of view.
Also:
1) The sorting example is O(n!) not because of limitations of the language, as the article suggests, but because the algorithm implemented is permutation sort, which is O(n!).
A typical sorting algorithm example in Prolog is merge sort which is as efficient in Prolog as merge sort can be. Here are a few sorting algorithms in Prolog, including merge sort and quick sort:
2) The Sudoku example uses a Constraint Logic Programming library implemented in Prolog (from the looks of it, Gnu Prolog). CLP is a different paradigm than plain logic programming, where one programs by specifying constraints.
A Sudoku solver in actual Prolog can be found in "99 Prolog Problems":
Out of order calculation based on dependencies: mlet (magic let/mutual let) macro:
This is the TXR Lisp interactive listener of TXR 212.
Quit with :quit or Ctrl-D on empty line. Ctrl-X ? for cheatsheet.
1> (mlet ((w 3)
(x (+ z w))
(z (* 2 w)))
(list x z w))
(9 6 3)
Obligatory macro-expansion:
2> (macroexpand '(mlet ((w 3)
(x (+ z w))
(z (* 2 w)))
(list x z w)))
(let (#:g0011 #:g0012
#:g0013)
(symacrolet ((w (force #:g0011))
(x (force #:g0012))
(z (force #:g0013)))
(set #:g0011
(delay 3))
(set #:g0012
(delay (+ z w)))
(set #:g0013
(delay (* 2 w)))
(list x z w)))
Circular dep naturally fails:
1> (mlet ((x y) (y z) (z x)))
nil
2> (mlet ((x y) (y z) (z x)) x)
** (expr-2:1) force: recursion forcing delayed form y (source location n/a)
the (delay y) expression is not in the scope of (symacrolet ((y #:g2)) ...). Local symbol macros are lexically scoped. They can shadow lexical variables and be shadowed by them and so on.
So y in (delay y) will not be expanded there as we need it to, which we need because the initializing expressions in mlet can refer to all the variables (including their own, if they are careful).
This is why the code binds all of the gensyms first, and then initializes them by assignment in a scope in which the symacrolets are all visible.
Using mlet plus some lazy structure like a lazy cons (lcons) we can do useful things:
1> (set *print-circle* t)
t
2> (mlet ((lc (lcons 1 lc))) lc) ;; make a circular list
#1=(1 . #1#)
> It’ll be very interesting to see if the symbolic programming model is as flexible as Wolfram claims and can truly take advantage of all of this data.
Wolfram could have implemented his large standard library also for any other ecosystem. The magic of this library (which goes along with Wolfram's Lisp dialect but is considered as a unit) is that it is extremely high level, allowing rapid application development. But as with most libraries, it could have been developed for any language/idiom, such as a traditional object oriented python.
My 2 cents is that Mathematica and the Wolfram language are great for computational exploration (Ex: optimization, solving equations, plotting, statistics, calculus...etc etc). I think all the stuff that they really like to sell (Ex: the knowledge engine) are a gimmick. Yeah it can tell me how many calories are in spaghetti, but honestly...who cares? Normally, you would just get that in a dataset anyway which is more transparent. All my data is extremely private too, and they'll never have it available.
The explorative character of the MMA/Wolfram language is probably mostly due to the "REPL on stereoids". IPython provides a similar attempt but is "traditional" OOP (with explorable documentation and members/methods). Therefore, I am not that sure about the unique selling point of Mathematica. From my POV it is the pure size of the library and thus power of expression evaluation, like finding the algebraic solution to a complicated integral.
The dependent types example seems underwhelming; rejecting arrays of unlike length at compile time is something I'd expect from a Pascal compiler from 1975.
How about C90: pointer to array of 10 is not compatible with a pointer to array 20:
int process_array(int (*pa)[20]);
int main(void)
{
int array[10];
process_array(&array);
return 0;
}
GCC:
array.c: In function ‘main’:
array.c:6:17: warning: passing argument 1 of ‘process_array’ from incompatible pointer type [-Wincompatible-pointer-types]
process_array(&array);
^
array.c:1:5: note: expected ‘int (*)[20]’ but argument is of type ‘int (*)[10]’
int process_array(int (*pa)[20]);
^~~~~~~~~~~~~
The goal is to get static time checking of dynamic types. For example, if I take two dynamic length arrays and loop n times, appending (optionally?) an element to each array, can you still provide a compile-time check that both arrays are necessarily the same length. It’s much more powerful than what you describe.
here's a full code example in Idris, demonstrating Dependent Types, that's not completely facile:
import Data.String
-- takes two integers, and a proof that x < y, and yields an integer
add :
(x : Integer) ->
(y : Integer) ->
(prf : x < y = True) -> -- require a proof that that x < y
Integer
add x y prf = x + y
main : IO ()
main = do
sx <- getLine -- read string from input
sy <- getLine -- read string from input
let Just x = parseInteger sx -- assuming int parse is ok, else error
let Just y = parseInteger sy -- assuming int parse is ok, else error
case decEq (x < y) True of -- decEq constructs a proof (prf) if x < y is True
Yes prf => print (add x y prf) -- yes, we got a prf, pass it to add
No => putStrLn "no prf, x is not less than y" -- the prf variable is not available in this case
lets say I mess up the sign of the comparison on the case line and write decEq (x > y) instead... then I'd get a type error
When checking argument prf to function Main.add:
Type mismatch between
x > y = True (Type of prf)
and
x < y = True (Expected type)
there's no way to construct the prf value artificially, or sneak in different parameters that are unrelated to the prf value.
Too bad Behavioral Programming isn’t discussed as I find it to be the most fascinating one especially because its main objective is to better align programming to how humans think: https://lmatteis.github.io/react-behavioral/
Wolfram always impresses me but I can't help but feel like it will never go anywhere. How can it grow without being crushed under its own weight? As he stated in the video, its all hand crafted data set munging to fit it all together.
I'd love to see a world where wolfrom pulls on datasets out in the wild much like a search engine scrapes web pages but is such a thing possible? It begins to sound like a SOAP/WSDL fever dream when you think about automatic knowledge integration.
Maybe something closer to the open source package managers? Wolfram datasets could specify interfaces and dependencies? At least that would allow for new and exciting datasets to gain adoption in the community.
I find it interesting that the discussion on Dependent Types lists Idris and Coq as languages and discusses Formal Verification but mostly focuses on Idris and Scala with Shapeless... but to my knowledge, Coq has actually won out in 2019 for this, and Coq has even branded itself for this specifically[0].
[0] https://coq.inria.fr/ - Coq is a formal proof management system.