Prelim question about Stanza type interfaces


igbi@...
 

Dear Patrick,

This is probably premature. I need to do some experiments with Stanza to see if can duplicate some past experiments that I've done in other programming languages, all of which have ultimately gotten the reject.

In this email, I'll mainly just do some talking. You can ignore any of it. I think I mainly need to write it to get some motivation. However, I'll ask two questions which most likely can be answered.

Q1: Will Stanza ever have something like interfaces or traits, so that the properties of a type can be specified, for the purposes of type inforcement? As an example, Google Dart now has a strong mode, which gives Dart an enforcement feature that it didn't have initially.

Q2: In chapter 4 of your book you say, "Types do not live inside functions, nor do functions live inside types." I need for a struct type to hold a lambda function as a field, to be initialized by the constructor. Can your struct do that, or something else? I'd think that I can easily find this out once I install the software.

*CONTEXT: trying to meld a programming language with standard mathDefinitions-naiveSets-algebraicStructures-andMoreSemiFormalism*

My B.S is in math, so I'm not really a programmer, but I started on the search for the mother-of-all-programming-languages about September 2013. Initially, it was supposed to be Scala.

I prefer for emails like this to serve some purpose and be "on topic". At the very least, maybe this email will show you that there's still room for more programming languages. In my search, four criteria have been good-market-share/good-backing, clean syntax, decent performance, and an amalgam of modern-language-features.

Obviously, you have no market share, so if I'm still looking at Stanza, it must mean something good, at least on paper, or PDF.

I've done proof-of-concept experiments with Rust, Dart, TypeScript, Julia, Python, Haskell-ish languages, and C++. Those gave me enough experience to think through things about the other established and new languages.

As to new languages, a competitor of yours, for my needs, would be Idris, a dependently-typed functional language. But the lack of a basic feature can turn me off, since there's so much risk as to whether a language will have any lasting power. Typical of many functional languages, Idris doesn't have an array/vector type as part of the standard distribution, so I give it the reject.

*Exposure to Proof Assistants as a game-changer*

One starting point for me was exposure to the type class structure of the Isabelle proof assistant.

A logic called Isabelle/HOL is the main logic of the Isabelle product. It's a language very similar to Haskell. In particular, it has what are called axiomatic type classes.

A PDF of most of the logic is in this PDF (click the link 'document'):

https://isabelle.in.tum.de/dist/library/HOL/HOL/index.html

Particular chapter for order, lattices, and algebra would be chapters 4, 5, 6, 10, 15, 16, and 17. Eventually, they build up to the real numbers formalized as Cauchy Sequences. For myself, I'd just like to tie in a language, such as Stanza, semi-formally for natural numbers, integers, and rational numbers.

Anyway, the type-class structure is what I'd call "fine-grained". Drawing from how they do things, to build up to something like an additive group, I'd define more types than many people would. One purpose would be to more closely follow the progression of a standard abstract algebra book, but not quite.

With the standard mathematics of the mind, there's no need to define a syntactic type like 'Zero', since there's only one type, 'set'.

Thanks for your time.

GB

Join lbstanza@groups.io to automatically receive all group messages.