diff --git a/Hasklet3.hs b/Hasklet3.hs new file mode 100644 index 0000000..1cb3d5a --- /dev/null +++ b/Hasklet3.hs @@ -0,0 +1,152 @@ +module Hasklet3 where + +import Data.Semigroup (All(..)) + + +-- | A list of pairs of elements of type a AND b. +data ListP a b + = NilP + | ConsP a b (ListP a b) + deriving (Eq,Show) + +-- | A list of elements of either type a OR b. +data ListE a b + = NilE + | ConsL a (ListE a b) + | ConsR b (ListE a b) + deriving (Eq,Show) + +-- | Containers with two different element types that can be mapped over. +-- +-- Instances of Bifunctor should satisfy the following laws: +-- * bimap id id <=> id +-- * bimap (f1 . f2) (g1 . g2) <=> bimap f1 g1 . bimap f2 g2 +-- +class Bifunctor t where + bimap :: (a -> c) -> (b -> d) -> t a b -> t c d + +-- | Test cases for Bifunctor instances. +-- +-- >>> bimap (+1) (>3) (ConsP 1 2 (ConsP 3 4 NilP)) +-- ConsP 2 False (ConsP 4 True NilP) +-- +-- >>> bimap (+1) even (ConsL 1 (ConsR 2 (ConsR 3 (ConsL 4 NilE)))) +-- ConsL 2 (ConsR True (ConsR False (ConsL 5 NilE))) +-- + +-- [Bifunctor instances go here.] + +instance Bifunctor ListP where + bimap f g NilP = NilP + bimap f g (ConsP a b r) = ConsP (f a) (g b) $ bimap f g r + +instance Bifunctor ListE where + bimap f g NilE = NilE + bimap f g (ConsL a r) = ConsL (f a) $ bimap f g r + bimap f g (ConsR b r) = ConsR (g b) $ bimap f g r + +-- | Map over the left elements of a bifunctor. +-- +-- >>> mapL (+5) (ConsP 1 2 (ConsP 3 4 NilP)) +-- ConsP 6 2 (ConsP 8 4 NilP) +-- +-- >>> mapL even (ConsL 1 (ConsR 2 (ConsR 3 (ConsL 4 NilE)))) +-- ConsL False (ConsR 2 (ConsR 3 (ConsL True NilE))) +-- +mapL :: Bifunctor t => (a -> c) -> t a b -> t c b +mapL = flip bimap id + +-- | Map over the right elements of a bifunctor. +-- +-- >>> mapR (+5) (ConsP 1 2 (ConsP 3 4 NilP)) +-- ConsP 1 7 (ConsP 3 9 NilP) +-- +-- >>> mapR even (ConsL 1 (ConsR 2 (ConsR 3 (ConsL 4 NilE)))) +-- ConsL 1 (ConsR True (ConsR False (ConsL 4 NilE))) +-- +mapR :: Bifunctor t => (b -> c) -> t a b -> t a c +mapR = bimap id + + +-- | Containers with two different element types that can be folded to +-- a single summary value. +class Bifoldable t where + bifoldr :: (a -> c -> c) -> (b -> c -> c) -> c -> t a b -> c + + +-- | Test cases for Bifoldable instances. +-- +-- >>> let addL x (y,z) = (x+y, z) +-- >>> let mulR x (y,z) = (y, x*z) +-- +-- >>> bifoldr addL mulR (0,1) (ConsP 1 2 (ConsP 3 4 NilP)) +-- (4,8) +-- +-- >>> bifoldr addL mulR (0,1) (ConsL 1 (ConsR 2 (ConsR 3 (ConsL 4 NilE)))) +-- (5,6) +-- + +-- [Bifoldable instances go here.] + +instance Bifoldable ListP where + bifoldr _ _ c NilP = c + bifoldr f g c (ConsP a b r) = f a $ g b $ bifoldr f g c r + +instance Bifoldable ListE where + bifoldr _ _ c NilE = c + bifoldr f g c (ConsL a r) = f a $ bifoldr f g c r + bifoldr f g c (ConsR b r) = g b $ bifoldr f g c r + +-- | Fold over the left elements of a bifoldable. +-- +-- >>> foldrL (+) 0 (ConsP 2 3 (ConsP 4 5 NilP)) +-- 6 +-- +-- >>> foldrL (*) 1 (ConsL 2 (ConsR 3 (ConsR 4 (ConsL 5 NilE)))) +-- 10 +-- +foldrL :: Bifoldable t => (a -> c -> c) -> c -> t a b -> c +foldrL = flip bifoldr (const id) + +-- | Fold over the right elements of a bifoldable. +-- +-- >>> foldrR (+) 0 (ConsP 2 3 (ConsP 4 5 NilP)) +-- 8 +-- +-- >>> foldrR (*) 1 (ConsL 2 (ConsR 3 (ConsR 4 (ConsL 5 NilE)))) +-- 12 +-- +foldrR :: Bifoldable t => (b -> c -> c) -> c -> t a b -> c +foldrR = bifoldr (const id) + +-- | Map each element in a bifoldable to a common monoid type and combine +-- the results. This function is used by the 'checkAll' and 'toEitherList' +-- functions below. +-- +-- >>> checkAll odd even (ConsP 1 2 (ConsP 3 4 NilP)) +-- True +-- +-- >>> checkAll odd even (ConsL 1 (ConsL 2 (ConsL 3 (ConsR 4 NilE)))) +-- False +-- +-- >>> toEitherList (ConsP 1 True (ConsP 2 False NilP)) +-- [Left 1,Right True,Left 2,Right False] +-- +-- >>> toEitherList (ConsL 1 (ConsL 2 (ConsL 3 (ConsR "hi" NilE)))) +-- [Left 1,Left 2,Left 3,Right "hi"] +-- +bifoldMap :: (Monoid m, Bifoldable t) => (a -> m) -> (b -> m) -> t a b -> m +bifoldMap f g = bifoldr (mappend . f) (mappend . g) mempty + +-- Jack tried doing it point free, so I did too! +-- bifoldMap = (.(mappend.)).flip flip mempty.bifoldr.(mappend.) + +-- | Check whether all of the elements in a bifoldable satisfy the given +-- predicates. The 'All' monoid used in the implementation is the boolean +-- monoid under conjunction. +checkAll :: Bifoldable t => (a -> Bool) -> (b -> Bool) -> t a b -> Bool +checkAll f g = getAll . bifoldMap (All . f) (All . g) + +-- | Create a list of all elements in a bifoldable. +toEitherList :: Bifoldable t => t a b -> [Either a b] +toEitherList = bifoldMap (\x -> [Left x]) (\y -> [Right y]) diff --git a/proposal_feedback.md b/proposal_feedback.md new file mode 100644 index 0000000..f7b5621 --- /dev/null +++ b/proposal_feedback.md @@ -0,0 +1,85 @@ +## 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.