@edwinbrady does idris use any especially interesting technique to elaborate implicit things like foralls and constraints?
-
-
Replying to @beka_valentine
Not really - for implicits it generates a metavariable, which will hopefully be solved in the course of solving unification problems. Auto implicits (constraints) are solved by a type driven search. I think it's fairly standard, in so far as there is a "standard" here at all.
1 reply 0 retweets 0 likes -
Replying to @edwinbrady
how does idris handle cases like M : forall a. B -> C a ~ B -> forall a. C a?? does it do re-abstraction as necessary or??
1 reply 0 retweets 0 likes -
Replying to @beka_valentine
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...)
2 replies 0 retweets 0 likes -
Replying to @edwinbrady
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 = f1 reply 0 retweets 0 likes
Oh, right, I see. Yes, in Idris you'd have to manually eta expand f to get the implicits in the right order.
-
-
Thanks. Twitter will use this to make your timeline better. UndoUndo
-
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.