3 ms·

I'm a complete buffoon when it comes to type theory. Would appreciate some help to understand what is going on here. I tried to search the article for a ration

by dgb23 5y ago

I'm a complete buffoon when it comes to type theory. Would appreciate some help to understand what is going on here. I tried to search the article for a rationale. I only found "beloved" and "elegant" as motivators. Can someone give me a clear, understandable rationale and example? What problem would higher kinded types solve in Rust? I have trouble thinking purely in terms of abstraction, when I can't relate a process to some kind of goal. I also thank the author for the "braindamage" warning. Unfortunately I already had a metaphorical stroke way before that. The author acknowledges that the exercise was "not attractive" in the end, because of syntactical noise and lack of coherent type checking. What would a correct and useful implementation of this achieve?

throwaway17_17 5y ago
I don’t know if I can do an example in a common enough syntax to make sense. However, the general/basic example for higher kinded types is usually a Collection<T> vs a List<T>. The List take some type T (i.e. int, float, char) and is a list of ‘objects’ of that type. Every ‘object in the list is an int. A Collection<T> is a collection of some type <T<T2>> (i.e. list<T>, option, vector<V>). This allows for the collection to be composed of ‘objects’ whose types are each some List<T> where each objects T can be different. So a Collection<List<T>> could be a list of [List<int>, List<float>, List<char>]. I think the jargony statement is that higher kinded types allow for a type to abstract over types which take another type as a constructor. From my perspective the rationale for higher kinded type is usually the drive/goal of having as high a ceiling for abstraction as possible and create ‘reusable’ and generic code over and above what is available without higher kinded types.
- dgb23 5y ago
 Ty! As the user of said collection: Are the underlying objects inferred when I look at them one by one?
 - throwaway17_17 5y ago
 I would not expect the T type in a Collection<List<T>> to be used in a way where inference would be an issue. Typically, the type system would use parametric polymorphism to just deal with the Collection and then probably ‘pattern-match’ on the type inside a list.
gpderetta 5y ago
Let's say you want to write a generic function to convert from a container type to another container type: linked_list<int> l; vector v = to_container(l); In C++ this would be: template<template<class...> class ResultT, range Range, class T = range_value_t<Range> > ResultT<T> to_container(Range range) { return ResultT<T>(begin(range), end(range)); } list<int> x = ...; vector y = to_container<vector>(x); Because of the lack of type inference (only a simple form of type deduction is available in C++)[1], we have to specify the kind of container we want in the call to to_container. We do not have to specify the value type though (int in this case), so the ResultT parameter of to_container is an HKT. Range_value_t is a type query to get the value_type of the range. It is used to initialize a default template parameter purely for syntactical convenience. This is C++ of course so things are always a bit more complex. In particular a template template parameter is not really a type which makes is harder to manipulate consistently. More advanced metaprogramming libraries prefer to use types with associated templated types instead, which are another form of HKT, but it is not needed for this case. There are also ways around having to specify vector in the call to to_container using a proxy result type and a templated conversion operator, but it is again overkill in this case. Finally note that C++ templates are by default untyped: only instantiations are type checked. We use concepts for the range parameter that at least allows type checking of the range parameter at the call site without full instantiation, but as far as I can tell there are still no higher kinded concepts. I believe that Rust doesn't have HKTs yet exactly because higher kinded concepts (called traits in rust) are hard to define. [1] whether languages with proper type inference can deduce HTKs is beyond my pay grade, but I assume they can.
- sargstuff 5y ago
 Problem isn't "whether languages with proper type inference can deduce HTKs". The issue for rust is in allowing HTKs; can the same rust language guardrails be guaranteed. C++ allows one to get at the underlying "bit patterns" The idea of Rusts gardrails is to prevent that. The more things that sit between the actual "bit patterns", the more ways there are to get at the actual underlying "bit patterns". Programmer defined HTKs add additional paths to the underlying bit patterns which may/maynot include inferences needed for rusts "fixed" guardrails.
rhdunn 5y ago
With class/object generics, you are abstracting over the type the class is operating on, so you can have a List<Int> or List<String>. The class can define a single implementation on all those types, and functions using that class can be written that also operate on any List instance (List<T>). If you have a function `f(A) -> B` (e.g. converting a String to an Integer), you can define a map operation that works on List<A> and returns a List by applying f to each item in List<A>. This map operation is useful for other objects (Optional, Set, Array, etc.). It is also the building block for other functions. Higher Kinded Types allow you to say you have some type F<T>, where F is a type (List, Array, etc.) that can operate on any instance of T in a way that you can vary T without varying F. You could then define map like: interface Mappable<A, F<A>> { fun map(f: (A) -> B): F } class List<T> : Mappable<T, List<T>> { fun map(f: (A) -> B): List { ... } } What category theory does is define a common language for these operations, and combined types -- which is where you get terms like Monad from. From a programming perspective, this is just an interface that implements several other interfaces, provides a set of methods an implementation must implement, and a set of methods the implementation gets "for free". -- This is similar to implementing Iterable, List, or other collection interfaces and getting a bunch of functionality for free.
- dgb23 5y ago
 > What category theory does is define a common language for these operations, and combined types This made it click thank you!
- deleted 5y ago
 [deleted]
ReleaseCandidat 5y ago
> What problem would higher kinded types solve in Rust? You don't have a way to say in Rust 'this functions works on types similar to an 'Option<T>' for all types T. Or 'this functions works on types similar to a 'LinkedList<T>' for all types T. Which actually is more or less the same, we can therefore name both 'Option' and 'LinkedList' for example, well, 'Mona'.

by dgb23 5y ago

throwaway17_17 5y ago

I don’t know if I can do an example in a common enough syntax to make sense. However, the general/basic example for higher kinded types is usually a Collection<T> vs a List<T>. The List take some type T (i.e. int, float, char) and is a list of ‘objects’ of that type. Every ‘object in the list is an int. A Collection<T> is a collection of some type <T<T2>> (i.e. list<T>, option, vector<V>). This allows for the collection to be composed of ‘objects’ whose types are each some List<T> where each objects T can be different. So a Collection<List<T>> could be a list of [List<int>, List<float>, List<char>]. I think the jargony statement is that higher kinded types allow for a type to abstract over types which take another type as a constructor. From my perspective the rationale for higher kinded type is usually the drive/goal of having as high a ceiling for abstraction as possible and create ‘reusable’ and generic code over and above what is available without higher kinded types.

dgb23 5y ago
Ty! As the user of said collection: Are the underlying objects inferred when I look at them one by one?
- throwaway17_17 5y ago
 I would not expect the T type in a Collection<List<T>> to be used in a way where inference would be an issue. Typically, the type system would use parametric polymorphism to just deal with the Collection and then probably ‘pattern-match’ on the type inside a list.

gpderetta 5y ago

Let's say you want to write a generic function to convert from a container type to another container type: linked_list<int> l; vector v = to_container(l); In C++ this would be: template<template<class...> class ResultT, range Range, class T = range_value_t<Range> > ResultT<T> to_container(Range range) { return ResultT<T>(begin(range), end(range)); } list<int> x = ...; vector y = to_container<vector>(x); Because of the lack of type inference (only a simple form of type deduction is available in C++)[1], we have to specify the kind of container we want in the call to to_container. We do not have to specify the value type though (int in this case), so the ResultT parameter of to_container is an HKT. Range_value_t is a type query to get the value_type of the range. It is used to initialize a default template parameter purely for syntactical convenience. This is C++ of course so things are always a bit more complex. In particular a template template parameter is not really a type which makes is harder to manipulate consistently. More advanced metaprogramming libraries prefer to use types with associated templated types instead, which are another form of HKT, but it is not needed for this case. There are also ways around having to specify vector in the call to to_container using a proxy result type and a templated conversion operator, but it is again overkill in this case. Finally note that C++ templates are by default untyped: only instantiations are type checked. We use concepts for the range parameter that at least allows type checking of the range parameter at the call site without full instantiation, but as far as I can tell there are still no higher kinded concepts. I believe that Rust doesn't have HKTs yet exactly because higher kinded concepts (called traits in rust) are hard to define. [1] whether languages with proper type inference can deduce HTKs is beyond my pay grade, but I assume they can.

sargstuff 5y ago
Problem isn't "whether languages with proper type inference can deduce HTKs". The issue for rust is in allowing HTKs; can the same rust language guardrails be guaranteed. C++ allows one to get at the underlying "bit patterns" The idea of Rusts gardrails is to prevent that. The more things that sit between the actual "bit patterns", the more ways there are to get at the actual underlying "bit patterns". Programmer defined HTKs add additional paths to the underlying bit patterns which may/maynot include inferences needed for rusts "fixed" guardrails.

rhdunn 5y ago

With class/object generics, you are abstracting over the type the class is operating on, so you can have a List<Int> or List<String>. The class can define a single implementation on all those types, and functions using that class can be written that also operate on any List instance (List<T>). If you have a function `f(A) -> B` (e.g. converting a String to an Integer), you can define a map operation that works on List<A> and returns a List by applying f to each item in List<A>. This map operation is useful for other objects (Optional, Set, Array, etc.). It is also the building block for other functions. Higher Kinded Types allow you to say you have some type F<T>, where F is a type (List, Array, etc.) that can operate on any instance of T in a way that you can vary T without varying F. You could then define map like: interface Mappable<A, F<A>> { fun map(f: (A) -> B): F } class List<T> : Mappable<T, List<T>> { fun map(f: (A) -> B): List { ... } } What category theory does is define a common language for these operations, and combined types -- which is where you get terms like Monad from. From a programming perspective, this is just an interface that implements several other interfaces, provides a set of methods an implementation must implement, and a set of methods the implementation gets "for free". -- This is similar to implementing Iterable, List, or other collection interfaces and getting a bunch of functionality for free.

dgb23 5y ago
> What category theory does is define a common language for these operations, and combined types This made it click thank you!
deleted 5y ago
[deleted]

ReleaseCandidat 5y ago

> What problem would higher kinded types solve in Rust? You don't have a way to say in Rust 'this functions works on types similar to an 'Option<T>' for all types T. Or 'this functions works on types similar to a 'LinkedList<T>' for all types T. Which actually is more or less the same, we can therefore name both 'Option' and 'LinkedList' for example, well, 'Mona'.