Add proposal feedback and Hasklet 3

This commit is contained in:
Danila Fedorin 2021-05-03 20:48:52 -07:00
parent 5c5f250e00
commit f21332c647
2 changed files with 237 additions and 0 deletions

Hasklet3.hs Normal file
View File

@ -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])

85 Normal file
View File

@ -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](,
which is the x-axis of the [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](;
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](, 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](; 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):
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