[feniv]

Seems like this is an extension of the Curry-Howard-Lambek isomorphism [1] relating type theory, logic and category theory together. I find that to be one of the most beautiful results in computer science and have been working on a practical language built on the same principles for a while (A mix of Haskell, Prolog and APL in a python-like language)

[1] https://en.m.wikipedia.org/wiki/Curry–Howard_correspondence

[Tabzz98]

Is there any online material on this language?

[feniv]

Not yet. I've specced it out, but still working on the implementation. Here's a hand-written example showing how you can specify the constraints to validate a Knight's tour. You can then enumerate over the types to get valid tours.

https://gist.github.com/Feni/d819f120a7d179bc472c94df9471e60...