86 lines
6.9 KiB
Markdown
86 lines
6.9 KiB
Markdown
|
## Lazy
|
||
|
Heyo! This sounds like a fun project (and I'm not at all biased by my own choice of final project). I'll be linking
|
||
|
stuff I mention here without second thought; you may very well be aware of the stuff I link, but it's easier
|
||
|
to just dump all the information into this post. Here are a few ideas for you:
|
||
|
|
||
|
* You talk about linear algebra and vectors, as well as supporting simple extensions like dot products. Matrices and vectors
|
||
|
are particularly interesting, in my view, because they can be indexed by their size! For instance, the 2x2 identity matrix
|
||
|
is not at all the same as the 3x3 identity matrix. Operations that work for one of these matrices do not necessarily work for the
|
||
|
other: the simplest example is probably matrix multiplication. If you choose to include the size of the matrix into its type information (ala `Matrix(3,3)`, which I think is
|
||
|
vastly superior to having a basic `Matrix` type), you run into an issue: what's the type of the `multiply` operation? The best way
|
||
|
to formulate it is probably as `(Matrix n m, Matrix m k) -> Matrix n k`. But note that `n`, `m`, and `k` are not type
|
||
|
parameters, but values! When terms can depend on values, you arrive at [dependent types](https://en.wikipedia.org/wiki/Dependent_type),
|
||
|
which is the x-axis of the [lambda cube](https://en.wikipedia.org/wiki/Lambda_cube). It would be interesting to see this
|
||
|
feature implemented into your type system!
|
||
|
|
||
|
* If you already carry around type information for your matrices, another interesting question is: what if I wanted a different algorithm
|
||
|
for a different matrix size? For instance, there's a fairly simple definition of a matrix determinant for a 2x2 matrix, while the general
|
||
|
case of a matrix determinant is a little bit more involved. C++ has this feature (changing implementation depending on the type)
|
||
|
in the form of [template specialization](https://en.cppreference.com/w/cpp/language/template_specialization);
|
||
|
more generally, this is an example of terms (functions, for instance) depending on types (the type of a matrix). This, I believe,
|
||
|
is an example of [ad hoc polymorphism](https://en.wikipedia.org/wiki/Ad_hoc_polymorphism), which falls under the y-axis of the
|
||
|
lambda cube linked above. If you are feeling particularly adventurous, you can try implementing this!
|
||
|
|
||
|
* I'm not sure if you should be worried about parsing when defining language extensions. A more interesting
|
||
|
question is, what _is_ an extension, and how much power does it have? Would writing an extension correspond
|
||
|
to writing a module in Haskell, or a class in Java? Or would it be more something along the lines
|
||
|
of Lips libraries, which can (if I remember correctly) modify the entire language when loaded?
|
||
|
If you want something like the latter, then you may be interested to know that Lisp programs
|
||
|
are [homoiconic](https://en.wikipedia.org/wiki/Homoiconicity); that is, they can effectively
|
||
|
manipulate their own code and definitions; perhaps extensions could build upon this to, well,
|
||
|
extend the language. For your ideas about extensible notation, you could check out Agda's and Coq's
|
||
|
(in that order) notation mechanisms, since they both seem quite powerful and fairly ergonomic.
|
||
|
|
||
|
* "The output type will be a Maybe value, so a run time error such as accessing an undefined variable will result in a Nothing being returned."
|
||
|
Consider using "Either LanguageError" (with LanguageError being a type you define), since it'll help you carry out more helpful information
|
||
|
to the user. I also recommend taking a look into the `Reader` and `Except` monad transformers, since the former can be
|
||
|
used to keep a stack trace, and the latter to cleanly short-circuit erroring evaluation.
|
||
|
|
||
|
## Purple Cobras
|
||
|
Hey! A graphics language sounds neat; was this at all influenced by Ian's recent demonstration of his shader
|
||
|
art and Haskell DSL?
|
||
|
|
||
|
* A totality checker sounds fascinating! Since you're writing a functional DSL, you'll probably
|
||
|
be using recursion as the bread and butter of your programs. You probably know this, but the Idris
|
||
|
and Coq totally checkers use structural recursion to ensure totality; you can only recurse
|
||
|
on values that were "unpacked" from the current arguments. This is fairly restrictive;
|
||
|
for instance, the following definition of `interleave` would be rejected by Coq's totality
|
||
|
checker (if I remember correctly; I last encountered this a couple of years ago):
|
||
|
|
||
|
```Haskell
|
||
|
interleave [] xs = xs
|
||
|
interleave (y:ys) xs = y : interleave xs ys
|
||
|
```
|
||
|
|
||
|
The issue in the above example is that `xs` is not unpacked from `y:ys`.
|
||
|
|
||
|
An alternative approach (that I heard of), is using SMT and SAT solvers to compute various
|
||
|
invariants about your code, and I suspect that termination _may_ be one of them. If you can
|
||
|
somehow assert (and verify via SMT/SAT brute force) that there's a function of your arguments that's always
|
||
|
decreasing (for instance, the sum of the lengths of xs and ys in the above example), you can probably
|
||
|
convince yourself that the recursion is not infinite, and that termination is possible.
|
||
|
|
||
|
* I'm _sure_ you're aware of this, since Ben was the one that suggested this week's reading
|
||
|
group paper, but linear types would be excellent for this! Modifying various pixels in a buffer
|
||
|
could be done in-place if that buffer is linearly typed, since you are then guaranteed that
|
||
|
the effect of your destructive in-place update is not felt anywhere else. I think that
|
||
|
this would be particularly useful when you work on composition: while the "low level" details
|
||
|
of what changes and what doesn't may be lost at the abstraction boundaries of the
|
||
|
shader programs being composed, a linearly typed output from one shader would give
|
||
|
the next shader in the pipeline enough information to continue using in-place operations.
|
||
|
|
||
|
* It seems like not worrying about "undefined" values falls out of using a functional
|
||
|
language. You certainly can't write an uninitialized variable in something like vanilla Haskell.
|
||
|
What exactly do you mean, then, about avoiding the use of undefined values in your language?
|
||
|
I'm not sure I understand this objective.
|
||
|
|
||
|
* "The process of data moving from vertex to fragment shader should be represented as a typeclass or Monad". Intuitively,
|
||
|
I'm not so sure about this. It seems to me like you're defining a language that translates into GLSL; in this
|
||
|
case, you need not _really_ care about how data is transferred from one place to the other. You certainly
|
||
|
care in the sense that you want your uniforms / attributes to match up between stages in the pipeline (forgive me
|
||
|
for any mistakes with the lingo, I haven't touched shaders for years), but the task of actually manipulating
|
||
|
the data / pixels is not yours; it is delegated to the graphics card that's interpreting the GLSL that you generate.
|
||
|
Thus, using a Moands to represent graphics data does not seem like the way to go; on the other hand,
|
||
|
I think you will find it very fruitful to use various Monads from the MTL to implement your type checking and
|
||
|
translation.
|