It was a nice talk by @reifyreflect, though, telling us about the tricks he did to get around the Haskell type system :) #nottrollinghonest
-
-
Replying to @edwinbrady
@edwinbrady@reifyreflect *ahem* :t take take : (m : Fin (S n)) -> (Vect n a) -> Vect (cast m) a 'cast'? 'cast' in a dependent-type system?1 reply 0 retweets 0 likes -
Replying to @geophf
@geophf@reifyreflect Look at the definition of cast before mocking..! It's total and type safe. (Also, I've changed the type of 'take' now)2 replies 0 retweets 0 likes -
Replying to @edwinbrady
@edwinbrady@reifyreflect ;) I like your aside most of all. ;) What? Me? Mock? :t cast cast : a -> b :t believe_me believe_me : a -> b2 replies 0 retweets 0 likes
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.