Where communities thrive


  • Join over 1.5M+ people
  • Join over 100K+ communities
  • Free without limits
  • Create your own community
People
Activity
Aaron Weiss
@aatxe
I think Neel's definition is much less fuzzy than "what vs how"
and it gets at what seems to me to be the really important distinction, namely how much of the execution model you "see."
segeljakt
@segeljakt
I'm wondering what the term is for languages which have the right level of abstraction for a specific problem domain, maybe it is best to call them domain-specific?
Aaron Weiss
@aatxe
that sounds reasonable
Olle Fredriksson
@ollef
regarding the remark about full beta reduction: are there any programming language implementations that do that, though?
segeljakt
@segeljakt
of declarativity
segeljakt
@segeljakt
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.
Olle Fredriksson
@ollef
I would call that 'pure'
segeljakt
@segeljakt
agreed :thumbsup:
John Li
@johnli0135
Doesnt this mean you could consider SSA to be declarative in that register allocation is a nontrivial instantiation of an existential quantifier?
Aaron Weiss
@aatxe
@ollef no implementation of a programming language is going to use full beta because full beta is super non-deterministic.
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).
Olle Fredriksson
@ollef
The reason I asked was because I thought you were arguing that functional programming in general is neelk-declarative because there's full beta, but I see now that's not what you were doing
Aaron Weiss
@aatxe
Yeah, OCaml and Haskell are definitely dependent on their evaluation order. :smile:
Olle Fredriksson
@ollef
Even languages that don't specify an evaluation order, like Agda, might be evaluation order dependent in practice due to performance concerns of existing library code.
Aaron Weiss
@aatxe
I think I might still be comfortable calling Agda or Gallina declarative though.
Olle Fredriksson
@ollef
because they fulfill Neel's definition or because it just feels right?
Aaron Weiss
@aatxe
I think I'd argue both.
The semantics of the languages have full beta (or at least, I'm fairly certain they do).
Saul Shanabrook
@saulshanabrook
@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!)
Brendan Zabarauskas
@brendanzab
oooh, groovy
Brendan Zabarauskas
@brendanzab
Weird graph-based core language for a dependently typed language: https://gist.github.com/brendanzab/63c2d42c41c95922c0ee98e6e7a10cbb
Brendan Zabarauskas
@brendanzab
ooh, interesrting
snything that stands out to you that you like?
segeljakt
@segeljakt
I don't know much about it yet, but I will investigate more :D
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.

segeljakt
@segeljakt
(besides Pikelet of course)
Brendan Zabarauskas
@brendanzab
@ollef do you do something special for (\a -> a) 3 in sixty?
like, inferring the type?
somebody on the /r/ProgrammingLanguages discord is asking
Olle Fredriksson
@ollef
Yeah, that can be inferred to Int (if 3 : Int)
Not sure if I do anything special though? It falls out from unifying the parameter, argument, and return types.
Olle Fredriksson
@ollef
Allowing lambdas in inference mode is perhaps a little bit special? :)
Brendan Zabarauskas
@brendanzab
Ah cool. More asking from the perspective of someone going from a purely bidirectional system. What would be the pathway to figuring out how to do that?
Olle Fredriksson
@ollef
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.
Brendan Zabarauskas
@brendanzab
ohhh right!
that's pretty easy actually!
amazing
sorry, it was not at all obvious :sweat_smile:
Olle Fredriksson
@ollef
:D