26 ms·

Love to see a real-world example of GRIN! trait Functor[A]: fun map[B](self, f: A -> B) -> Self[B]; This looks a little wacky to me. I see that you

by Twey 2mo ago

Love to see a real-world example of GRIN! trait Functor[A]: fun map[B](self, f: A -> B) -> Self[B]; This looks a little wacky to me. I see that you can write HKTs in their η-long form and refer to them unapplied (`Functor`). But I don't understand how I would use this syntax to attach something to the trait that _doesn't_ depend on `A`. For (a silly) example, trait SizedFunctor[A]: Functor[A]: type Size; fun size(self) -> Size; How do I know that `List[A]::Size` is the same type as `List[B]::Size`? Relatedly, I want to read `Self` in there as ‘the thing that implements `Functor[A]`’ (e.g. List[A]`), but that makes `Self[B]`, instantiated, mean `List[A][B]`, which I think should be a kind error.

the_unproven 2mo ago
`Self` isn't the applied type (`List[A]`), rather it's the type constructor of kind `* -> *` constrained by `Functor`. In the map example it gets desugared into: fun map[Self: Functor, A, B](self: Self[A], f: A -> B) -> Self[B]; Since `Self` is the unapplied constructor, `Self[B]` just means `Functor[B]` e.g. `List[B]` not `List[A][B]`. The example you've shown with `SizedFunctor` is not currently supported, as support for associated types is not yet implemented. I got it on the roadmap tho!
- wavemode 2mo ago
  How do you define a trait that is itself generic? Like: trait ConvertTo[T]: fun convert(self) -> T; Seems to create a single trait ConvertTo, for a generic type with a [T] argument, rather than allowing one to define separate implementations for ConvertTo[i32], ConvertTo[String], etc.
- Twey 2mo ago
  Right, I got the notion — but syntactically I expect `Self` to refer to the thing named at the top of the block, which is a `Functor[A]`. I think what both I and the sibling comment are getting at is that there is a difference between `Functor : (Self : * → *) → Class` and `Functor : (Self : * → *) → (A : *) → Class`/preapplied `Functor : (Self : *) → Class` and the syntax seems to merge the two (using syntax for the latter that is automatically abstracted to the former). But it's not clear to me that you can do that without losing the ability to express some things. The associated type is a pointed example because the unwanted dependence breaks type equality, but consider also an associated function that should _not_ be parameterized by `A`.
  - the_unproven 1mo ago
    Fair point, I don't disagree with the statement that `Self` can be limiting as the trait is defined for `Functor[A]`. Thus imposing limitations on type system. You would want for type variable to not be attached directly to a type class on its definition? But still treated as a container type. Something like: trait Functor: fun fmap[A, B](f: A -> B, c: Self[A]) -> Self[B]; ... impl Functor for List[A]: fun fmap[A, B](f: A -> B, l: List[A]) -> List[B] List::fold(l, Nil[B], (t, h) => Cons(f(h), t)) ... The above would compile, but the Functor wouldn't be treated of a higher kind in the type-system. I'll try to work a flexible solution, thanks for the great callout!
    - Twey 1mo ago
      Right, so the definition of higher-kinded types is that the _parameter_ to the trait (here, `Self`) is higher-kinded (here, `* → *`) not that the trait is parameterized. So `impl Functor for List[A]` is not (semantically) correct: it's not `List[A]` that implements `Functor` but `List` itself.†‡ The important thing you get out of that is precisely the ability to talk about these kinds of universals: you can associate items to the type constructor itself before its eventual parameter is even in scope, and so the value of all such things must be the same independent of the parameter ‘for free’. As soon as you introduce the type parameter you incur a proof burden if you want to claim that the associated item is the same regardless of the value of the parameter, because you have introduced the syntactic possibility that they could vary. † There's an encoding of higher-kinded types in some languages that don't really have them as first-class citizens (e.g. Rust with associated type constructors) that does this by adding a ‘rewrap’ item to the trait: you implement `Functor` for `List<A>`, but also (as part of the trait) includes a type constructor `Rewrap<B> = List<B>`. This lets you encode the fact that the `Functor` instance is defined for `List<A>` for all values of `A`, but you still struggle to prove that some of their items are independent of the choice of `A`. ‡ To see both of these side-by-side, consider the instance for pairs, which are functorial in their right parameter (as well as the left parameter: they are bifunctorial, but that's not relevant here). So if you have a curried pair type constructor `Pair : * → * → *` it really is true that `Pair[A]`, not `Pair`, is a `Functor`: impl Functor for Pair[A]: fun fmap[B, C](f: B -> C, self: Pair[A][B]) -> Pair[B][C]): Pair(self.0, f(self.1))

by Twey 2mo ago

the_unproven 2mo ago

`Self` isn't the applied type (`List[A]`), rather it's the type constructor of kind `* -> *` constrained by `Functor`. In the map example it gets desugared into: fun map[Self: Functor, A, B](self: Self[A], f: A -> B) -> Self[B]; Since `Self` is the unapplied constructor, `Self[B]` just means `Functor[B]` e.g. `List[B]` not `List[A][B]`. The example you've shown with `SizedFunctor` is not currently supported, as support for associated types is not yet implemented. I got it on the roadmap tho!

wavemode 2mo ago
How do you define a trait that is itself generic? Like: trait ConvertTo[T]: fun convert(self) -> T; Seems to create a single trait ConvertTo, for a generic type with a [T] argument, rather than allowing one to define separate implementations for ConvertTo[i32], ConvertTo[String], etc.
Twey 2mo ago
Right, I got the notion — but syntactically I expect `Self` to refer to the thing named at the top of the block, which is a `Functor[A]`. I think what both I and the sibling comment are getting at is that there is a difference between `Functor : (Self : * → *) → Class` and `Functor : (Self : * → *) → (A : *) → Class`/preapplied `Functor : (Self : *) → Class` and the syntax seems to merge the two (using syntax for the latter that is automatically abstracted to the former). But it's not clear to me that you can do that without losing the ability to express some things. The associated type is a pointed example because the unwanted dependence breaks type equality, but consider also an associated function that should _not_ be parameterized by `A`.
- the_unproven 1mo ago
  Fair point, I don't disagree with the statement that `Self` can be limiting as the trait is defined for `Functor[A]`. Thus imposing limitations on type system. You would want for type variable to not be attached directly to a type class on its definition? But still treated as a container type. Something like: trait Functor: fun fmap[A, B](f: A -> B, c: Self[A]) -> Self[B]; ... impl Functor for List[A]: fun fmap[A, B](f: A -> B, l: List[A]) -> List[B] List::fold(l, Nil[B], (t, h) => Cons(f(h), t)) ... The above would compile, but the Functor wouldn't be treated of a higher kind in the type-system. I'll try to work a flexible solution, thanks for the great callout!
  - Twey 1mo ago
    Right, so the definition of higher-kinded types is that the _parameter_ to the trait (here, `Self`) is higher-kinded (here, `* → *`) not that the trait is parameterized. So `impl Functor for List[A]` is not (semantically) correct: it's not `List[A]` that implements `Functor` but `List` itself.†‡ The important thing you get out of that is precisely the ability to talk about these kinds of universals: you can associate items to the type constructor itself before its eventual parameter is even in scope, and so the value of all such things must be the same independent of the parameter ‘for free’. As soon as you introduce the type parameter you incur a proof burden if you want to claim that the associated item is the same regardless of the value of the parameter, because you have introduced the syntactic possibility that they could vary. † There's an encoding of higher-kinded types in some languages that don't really have them as first-class citizens (e.g. Rust with associated type constructors) that does this by adding a ‘rewrap’ item to the trait: you implement `Functor` for `List<A>`, but also (as part of the trait) includes a type constructor `Rewrap<B> = List<B>`. This lets you encode the fact that the `Functor` instance is defined for `List<A>` for all values of `A`, but you still struggle to prove that some of their items are independent of the choice of `A`. ‡ To see both of these side-by-side, consider the instance for pairs, which are functorial in their right parameter (as well as the left parameter: they are bifunctorial, but that's not relevant here). So if you have a curried pair type constructor `Pair : * → * → *` it really is true that `Pair[A]`, not `Pair`, is a `Functor`: impl Functor for Pair[A]: fun fmap[B, C](f: B -> C, self: Pair[A][B]) -> Pair[B][C]): Pair(self.0, f(self.1))