A friendly little systems language with first-class types. https://github.com/pikelet-lang
and it gets at what seems to me to be the really important distinction, namely how much of the execution model you "see."
the definition in this book confuses me http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.102.7366&rep=rep1&type=pdf
of declarativity
We say the operation is declarative if, whenever called with the same arguments, it returns the same results independent of any other computation state. Figure 3.1 illustrates the concept. A declarative operation is independent (does not depend on any execution state outside of itself), stateless 1 (has no internal execution state that is remembered between calls), and deterministic (always gives the same results when given the same arguments). We will show that all programs written using the computation model of the last chapter are declarative.
full beta in a lambda calculus means, more or less, that you can evaluate absolutely anywhere whenever you want and in any order.
in an implementation, you'll realize this by... well, picking one evaluation order.
(to clarify, I really do mean anywhere, including arbitrarily evaluating as much as possible under a binder or several)
but I think that's precisely what makes a lambda calculus with full beta feel declarative by Neel's definition.
that is: there's an existential quantification in every rule relating to the decomposition of expressions into the expression to reduce and its evaluation context, and the instantiation is nontrivial since decomposition is not unique (and indeed, most sufficiently complex expressions will have a lot of decompositions).
The semantics of the languages have full beta (or at least, I'm fairly certain they do).
@brendanzab Not sure how related, but I have also been experimenting with JSON representations for a System F language: https://github.com/Quansight-Labs/metadsl/blob/2ee12dc51c3decb915c4fa781400f03e687d1f4f/typez/src/schema.ts#L161-L182
No the actualy definitions, just like the types, and functions. Then you can pair that with a normalized form of an expression, and start to talk about this is some form in this context.
(If this has already been done before, would love to see examples of it!)
Weird graph-based core language for a dependently typed language: https://gist.github.com/brendanzab/63c2d42c41c95922c0ee98e6e7a10cbb
snything that stands out to you that you like?
I have seen this array programming language also http://www.sac-home.org/doku.php?id=docs:tutorial
the language I'm the most excited about is this https://github.com/miking-lang/miking/tree/develop
Miking (Meta vIKING) is a meta language system for creating embedded domain-specific and general-purpose languages.
Miking is not a programming language, but rather a language system for creating languages and generating efficient compilers.
like, inferring the type?
somebody on the /r/ProgrammingLanguages discord is asking
Not sure if I do anything special though? It falls out from unifying the parameter, argument, and return types.
With the usual bidirectional set up where you have an
infer and a check function, you can quite flexibly add more cases to one or the other. Specifically for inferring lambdas, you can invent two meta variables and then check the lambda against m1 -> m2 (or just invent one for the parameter and infer the body assuming that, which is the HM way to do it). You can do the same with dependent types but then you'll only infer non-dependent functions because m2 can't depend on the argument. If you want to allow inferring dependent functions, you make it (x : m1) -> m2 x.
that's pretty easy actually!
amazing
sorry, it was not at all obvious :sweat_smile: