@edwinbrady does idris use any especially interesting technique to elaborate implicit things like foralls and constraints?
Is this about the second 'a'? That'd be a new variable, just as if it had a different name. Or do you mean something else? (embarrassingly I can't remember what the ~ means just now...)
-
-
i de ides to test it out in ideas and to my surprise it actually doesn’t do what i thought it would
bad : ({a : Type} -> Bool -> a -> a) -> Bool -> {a : Type} -> a -> a
bad f = f -
Oh, right, I see. Yes, in Idris you'd have to manually eta expand f to get the implicits in the right order.
- 1 more reply
New conversation -
-
-
isomorphism! i guess
-
see other tweet. but compare that to haskell which is fine with doing good :: (forall a. Bool -> a -> a) -> Bool -> forall a. a -> a good f = f
End of conversation
New conversation -
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.