I don't understand the interactions between records and implicit parameters in #idris. Why can't I manually set the declared implicit parameters of a record's field outside the record's declaration?

@mavaxavou Can you give an example? I don't know what you mean by implicit parameters of a record's field.

@falsifian I'll give it a try. I wanted to define a category. So I defined a record, containing the field object, which is the type of the category's objets. Then a field morphism, which has type object -> object -> Type.

After that, I added a field compose, which build a morphism from two morphisms. It's type is thus compose : {a, b, c : object} -> morphism a b -> morphism b c -> morphism a c.

So far so good, it does what I want. But, if I write a function that takes a category, let's call it cat, and do stuff, I can't manually specify the implicit parameters a, b and c of the function compose cat. Which is ok most of the time, but in rare cases, I would like to be able to specify them.


@mavaxavou I haven't used Idris 1 in a while. Anyway, not sure if I'm understanding what you're trying to do; LMK.

· · Web · 0 · 0 · 0
Sign in to participate in the conversation
Mastodon @ SDF

"I appreciate SDF but it's a general-purpose server and the name doesn't make it obvious that it's about art." - Eugen Rochko