search

sleexyz / hylogen

GLSL embedded in Haskell
https://hylogen.com
481 stars 25 forks source link

Vector concat #61

Open sleexyz opened 8 years ago

sleexyz commented 8 years ago 
(:+) :: forall (n :: Nat) (m :: Nat). (Veccable n, Veccable m) 
     => Vec n -> Vec m -> Vec (n + m)
mdaiter commented 8 years ago

Like this? http://docs.idris-lang.org/en/latest/tutorial/typesfuns.html#vectors

+1 for this feature. Hit me up if you want to work on this together (I'm getting more into Idris/Agda programming and category theory too these days :) I'd love to help out. )

sleexyz commented 8 years ago

yeah! it should be fairly easy. There just needs to be a way to reify a term from a 'Nat' at the type level, maybe with typeclasses? Perhaps i already have the mechanisms in place, haven't touch this project in a month. But feel free to poke around, let me know if you have questions!

(yeah, getting into Agda!)