Albert ten Napel
Albert ten Napel
Thanks for the reply! Yeah type classes is exactly the reason why I became interested in Qualified types, thanks for the paper suggestion!
Yeah that's what I thought. I wonder if you could look at how type variables appear in the ADT and tag the type variables with their variance (invariant, co- contravariant...
Thanks, I will look in to `Coercible`. Does that mean in the case of `f a
Thanks! I hadn't thought of it like that, that does make it clearer for me as well :)
I think Agda only allows covariant type constructors. In Haskell though non-covariant datatypes are used, so it might be very restrictive (for example Fix). I'm pretty sure just adding that...
Oh sorry, yes you are very right. You need to perfom kind checking. There already is a well-formedness check for types in the system, so that check could also do...
Is there any progress on this? We are currently using the checkstyle xml report that Scalastyle outputs and we are working on switching to Scalafix.
I recommend going through ["Software Foundations"](https://softwarefoundations.cis.upenn.edu/). It teaches theorem proving in Coq. The learning curve is not too steep if you know a bit of programming. For the implementation of...
My attempt at this: ``` interface Pair { fst: A; snd: B } const pair = (fst: A, snd: B): Pair => ({ fst, snd }); type Lens = (val:...
So that means you know a way to implement this that would not force the user to write down the type arguments explicitly every time?