Gabriel439

8 ms·

31.
by Gabriel439 7y ago
Author here: the syntax is inspired by all three of Haskell/PureScript/Elm
32.
by Gabriel439 8y ago
Author here: This is correct. I'm just borrowing a Haskell convention. Also, I like this convention because it leads to vertical alignment of commas.
33.
by Gabriel439 8y ago
This explains the disadvantages of using a general-purpose programming language as a configuration language: https://github.com/dhall-lang/dhall-lang/wiki/Safety-guarant...
34.
by Gabriel439 8y ago
You can do more than just compare the output of two programs in Dhall. You can verify using a semantic integrity check that two programs are the same for all possible inputs. For example: $ dhall hash <<< 'λ(x : Natural)
35.
by Gabriel439 8y ago
There are ASCII equivalents. You can type `\` instead of `λ` and `forall` instead of `∀`. Also `dhall format` will automatically translate ASCII to Unicode for you. However, if you do want to type them then see: https://en.wiki
36.
by Gabriel439 8y ago
Dhall's lists are homogeneous lists, meaning that every element always has the same type of value. This is true whether or not you annotate list elements with a type or you annotate the list with a type. You only need to annotate the
37.
by Gabriel439 8y ago
> What if the host executing the script had access to some intranet site with sensitive data? Would I be able to do a network import of such a URL, load it as raw text, and provide that as a header to another import? Yes, a local import
38.
by Gabriel439 8y ago
Author here: You might be interested in this post on safety guarantees: https://github.com/dhall-lang/dhall-lang/wiki/Safety-guarant... The main risks in executing potentially malicious Dhall code that is no
39.
by Gabriel439 8y ago
Author here: I opened an issue to track this request and remind myself to do this: https://github.com/dhall-lang/dhall-lang/issues/189
40.
by Gabriel439 9y ago
The way I would phrase it is that you've concentrated your input and output sanitisation in a trusted kernel (i.e. the compiler/interpreter) and that puts an upper bound on the amount of code that you need to audit (just the compi
41.
by Gabriel439 9y ago
Yes, but it's a restricted set of input and output: the only thing you can do is import other code. You can't, say, launch missiles or delete files unless the compiler/interpreter allows it
42.
by Gabriel439 9y ago
However, the compiler/interpreter places an upper bound on the amount of code that we need to audit because it acts like a trusted kernel. We only need to audit the compiler/interpreter itself for safety and once we do so we can
43.
by Gabriel439 9y ago
Yes, that's a good analogy However, I think the more important thing I'm trying to fix is how we compose code. The Rube-Goldberg machine the post refers to is the complicated mechanisms we have to deal with for combining code fra
44.
by Gabriel439 9y ago
There are two separate questions here: * "Why should we limit I/O to the compiler"? Think of the compiler or interpreter as a small trusted kernel. It's a mostly fixed code base that you can inspect and audit. The prog
45.
by Gabriel439 9y ago
To clarify: the idea is that both the view and controller are built into the interpreter. The interpreted program builds the model and is written in a a purely functional and effect-free language
46.
by Gabriel439 9y ago
Right, and where I'm going with this is that we should take the JavaScript model to its natural conclusion and use it more pervasively in other domains. In other words, more applications and domains should be configured via sandboxed
47.
by Gabriel439 9y ago
Yes, this entails moving more logic into compilers/interpreters. For example, Dhall is actually designed this way: not only is it a command line interpreter but it's also a Haskell library that you can use to interpret Dhall expr
48.
by Gabriel439 9y ago
To make an analogy to Python: you don't need to recompile Python to interpret new Python programs. Chrome would be like Python: Chrome is itself a compiled program, but it interprets user settings and web pages. Chrome is allowed to d
49.
by Gabriel439 9y ago
Your program can be a pure function which somebody else can invoke, so it's not necessarily a constant However, Dhall does have the ability to normalize under lambda when possible so it will actually do this for you if it can! For exa
50.
by Gabriel439 9y ago
The primary distinction from a dynamic language is that Dhall is typed, total, and does not permit arbitrary effects (only importing other code is allowed), so it's safe to evaluate arbitrary remote code and it's also safe to use
51.
by Gabriel439 9y ago
A closer analogy to Dhall would be if web pages were assembled entirely from JavaScript instead of HTML, URLs were just pointers to Javascript expressions, and JavaScript code could refer to other JavaScript code anywhere within the syntax
52.
by Gabriel439 9y ago
In Dhall's case it is a typed interpreter. So every time you interpret an expression there are three phases: * Resolve all imports (transitively, if necessary) * Type-check the code * Normalize the code (a.k.a. evaluation, but it can
53.
by Gabriel439 9y ago
Inputs in a purely functional world are limited to things that you can serialize and deserialize, which does not include functions or types. If you ingest values via imports instead of via traditional I/O then you can transmit any lan
54.
by Gabriel439 9y ago
I don't want to think about I/O. That's the point I want to focus on connecting pure code together without thinking about the details of how that happens. I want this for the same reason that I don't want to think abou
55.
by Gabriel439 9y ago
Author here: this is written for a primarily functional audience who already take for granted that it's good to minimize effects, but let me try to rephrase it another way for people who don't have that background Typically there
56.
by Gabriel439 9y ago
Dhall does the dumbest thing possible to enforce totality: Dhall doesn't support recursion! Note that Dhall does support lists and folds on lists (which are total), but not user-defined recursion For example, if you write: let
57.
by Gabriel439 9y ago
For the purposes of evaluation, it's still an improvement to have a total language. As I mentioned in another thread, using a totality checker is like wearing seatbelts: it doesn't protect against everything, but it's still
58.
by Gabriel439 9y ago
The latter example you gave will still not type-check in Dhall, although I'll still answer the spirit of your question You can write expressions in Dhall that will take a long time to evaluate (see the Ackerman example elsewhere in thi
59.
by Gabriel439 9y ago
Yes, however standardizing the language is higher priority at the moment
60.
by Gabriel439 9y ago
System Fw cannot type-check self application The type system is what prevents System Fw from being Turing complete. Specifically, the key bit is that you cannot unify the type "a -> b" with "a" (which is what prevent

More ›