Live data from Hacker News

Free-types: Higher kinded types in TypeScript

github.com

41–50 of 51 posts

Re: Free-types: Higher kinded types in TypeScript

#41
post #15

I wonder if there is any relationship between HKT and C#/Rust generics, from my perspective I always see HKT as "A type that accepts types that generates another type" and generic as "A functor that accepts types that generates another type". That makes me wonder if types and functors are exchangable.

It's easier to make the parallel between type-level and value-level reasoning. 1 is a value, and int is a concrete type. function increment(x) { return x + 1 } is a value-level function. You feed it a value x and you get a value back. List is a type-level function: you give it a concrete type T, you get another type back. function applyTwice(f, x) { return f(f(x)) } is a higher-order function that takes a functions a…

Finally an explanation that makes sense. Thank you :)

Re: Free-types: Higher kinded types in TypeScript

#42

Earlier quoted context omitted.

"a dependent function may depend on the value (not just type) of one of its arguments" from wikipedia https://en.wikipedia.org/wiki/Dependent_type The value does not exist during compilation. AFAIKT dependent type are used mostly during executable proof checkers to verify claims on the value-dependent types. So maybe using the term runtime is a bit to specific, but you do not have values (except literals) during type…

The "value" in this case is symbolic, sort of like defining an array with variable length arr[x] and having the compiler verify that arr[x+5] is always out of bounds before knowing the actual value of x. If the type system is not powerful to prove correctness of some expression, you will need to insert a runtime check that lets the compiler to trust the value at compile time.

You still need a way of normalizing expressions that is consistent with your runtime. To say that types ((x: bool) => F) and ((x: bool) => F) are the same, wrt judgemental equality, requires normalizing both to ((x: bool) => F).

Re: Free-types: Higher kinded types in TypeScript

#43

Earlier quoted context omitted.

"A type that accepts types that generates another type" is called a type constructor. And a "kind" is the type of a type constructor, just to have a new name and not needing to call that "type" too. "Generic types" like `Vec ` (in Rust) are type constructors, they "generate" a type `Vec ` from the type `T`. Type constructors that take one type as argument have the kind `* -> *` (or as Rust-y notation `fn(*) -> *` - r…

Edit2: oh, I guess misunderstood "A type that accepts types that generates another type". If you meant to say "A type that accepts (types that generates another type)", so a type constructor that accepts type constructors and not "(A type that accepts types) that generates another type", which is a type constructor.

Yeah, I think "types that generateS" is either a typo or sloppy English; it should be "types that generate".

I often wonder why it's so common for programmers with an acute awareness and mastery of syntax and grammar in programming languages to just throw all that precision and attention to detail out the window when it comes to natural language.

Re: Free-types: Higher kinded types in TypeScript

#44
post #18

Are these like type classes?

They are related, but different concepts. An HKT is the type of a type constructor. An example described in another comment in this thread is if you want to define the map function on any collection C (in pseudo-Java),

    C map(C coll, Function fun)
Mapping over an Array would return an Array while mapping over a List would return a List. C here is an HKT, the type of a type constructor with one argument.

In OOP a class is a description of what an object can do, often with a constructor that produces instances of the class with values as arguments. A type class is the same thing, but the constructor of a type class takes types as arguments. Type classes are useful because they allow defining functions for many types that share something without having to make the types inheritors of a common class (composition over inheritance basically).

For the example above I could define (pseudo Java) a type class like this,

    interface Mappable {
      C map(C coll, Function fun);
    }
and then if I want to define a function generic over anything that has a map I can do so by requesting both the thing and a Mappable of the thing,

     C foo(Mappable inst, C coll)
Then I can use the Mappable instance to call map over any coll instances. For example a generic "size" function could be defined like this [1],

    C foo(Mappable inst, C coll) {
      var out = 0;
      inst.map(coll, k -> {out++; return k});
      return out;
    }
So that function would be enough to prove that Mappable implies that C has a size and you can then define a function that gives you Sizeable from Mappable, which is useful composition.

The example above is very boilerplate heavy because Java doesn't really support type classes but in Scala and especially Haskell the syntax is a lot cleaner.

[1] Usually you would use a fold here instead of a side effecting map.

Re: Free-types: Higher kinded types in TypeScript

#45
post #15

Earlier quoted context omitted.

It's easier to make the parallel between type-level and value-level reasoning. 1 is a value, and int is a concrete type. function increment(x) { return x + 1 } is a value-level function. You feed it a value x and you get a value back. List is a type-level function: you give it a concrete type T, you get another type back. function applyTwice(f, x) { return f(f(x)) } is a higher-order function that takes a functions a…

Finally an explanation that makes sense. Thank you :)

In case you're wondering: Where this becomes incredibly powerful is in how it relates to ad-hoc polymorphism. Again, imagine this is pseudo-java.

    // Alternative one: subtype polymorphism. You have to implement Format as part of your type.
    interface Format { String format() }
    
    void printAll(things List) { things.forEach(thing => print(thing.format())) }

    // Alternative two: ad-hoc polymorphism. You can implement Format separately from the type you're implementing it for
    interface Format { String format(T t) }
    
    void printAll(things List, Format formatter) { things.forEach(thing => print(formatter.format(thing))) }
Doing ad-hoc polymorphism manually like this is obviously annoying as hell, it's the equivalent of doing dynamic dispatch in C by explicitly passing around vtables, but e.g. Haskell and Rust have direct support for ad-hoc polymorphism through typeclasses and traits respectively. Scala's implicits still require some amount of faffing about, but still make things much easier.

The bit where HKTs come in is when you want to have your interfaces talk about generics:

    // HKT goes here ----V
    interface Iterable> { forEach(C collection, Consumer fn) }
    
    
    void printAll(things List, Format fmt, Iterable iter) { iter.forEach(things, thing => print(fmt.format(thing))) }

Re: Free-types: Higher kinded types in TypeScript

#46

Earlier quoted context omitted.

> The thing is, it takes a bit of experience to appreciate why HKT are important, and typically you can only get this experience using Haskell. They're fairly common in Scala too, and I believe in OCaml through modules.

And C++ if you squint hard enough.

and F# with computations Seems common with functional programming, that it takes a mind-set change before seeing the need.

Re: Free-types: Higher kinded types in TypeScript

#47
post #18

Are these like type classes?

They are related, but different concepts. An HKT is the type of a type constructor. An example described in another comment in this thread is if you want to define the map function on any collection C (in pseudo-Java), C map(C coll, Function fun) Mapping over an Array would return an Array while mapping over a List would return a List. C here is an HKT, the type of a type constructor with one argument. In OOP a class…

> An HKT is the type of a type constructor.

That is a ("normal") kind `* -> *`. A Java `List` or `Set` would be a "normal/concrete" type constructor. In your example the problem is that `C` is a "generic" type constructor, so it has a higher (-order) kind, that takes a type constructor as argument (like `List` or `Set`) and constructs a type from this: `(* -> *) -> *`.

Re: Free-types: Higher kinded types in TypeScript

#48
post #25

Earlier quoted context omitted.

> No. Typescript cannot access runtime values (I assume you mean types that depend on runtime values). That's not the meaning of dependent types, and dependent type checkers don't require runtime information.

"a dependent function may depend on the value (not just type) of one of its arguments" from wikipedia https://en.wikipedia.org/wiki/Dependent_type The value does not exist during compilation. AFAIKT dependent type are used mostly during executable proof checkers to verify claims on the value-dependent types. So maybe using the term runtime is a bit to specific, but you do not have values (except literals) during type…

Well, I can't be bothered to edit wikipedia, but it's a confusing claim. Dependent typing does not require runtime information, results can be produced at compile time. The dependent type depends on a value, but the interesting property of the value is independently tracked in the type system, it's not retrieved from runtime information.

The gist of how it works is so:

    createEmptyIntList() => List {...}
    push(List) => List {...}
    firstElement(List | a > 0) => b {...}
In this example, you don't need to know runtime values, you need to know that you can safely get the first element. For that, you just need to know that something has been pushed at least once in the list.

Since push returns a type that is different from createEmptyList, your typesystem has this information.

Re: Free-types: Higher kinded types in TypeScript

#49
post #20
post #16

Earlier quoted context omitted.

Not really possible, because Record and Map aren't compatible at all. At best they both have something like `toString`. You'll need to define at least something like RecordFunctor and MapFunctor to make this useful.

Only if you want to abstract over them at usage-site. In my case I only ever used the concrete types and converted between them at some point.

Oh, so it's just a type alias for readability. Then it makes sense.

Re: Free-types: Higher kinded types in TypeScript

#50

Earlier quoted context omitted.

They are related, but different concepts. An HKT is the type of a type constructor. An example described in another comment in this thread is if you want to define the map function on any collection C (in pseudo-Java), C map(C coll, Function fun) Mapping over an Array would return an Array while mapping over a List would return a List. C here is an HKT, the type of a type constructor with one argument. In OOP a class…

> An HKT is the type of a type constructor. That is a ("normal") kind `* -> *`. A Java `List ` or `Set ` would be a "normal/concrete" type constructor. In your example the problem is that `C` is a "generic" type constructor, so it has a higher (-order) kind, that takes a type constructor as argument (like `List ` or `Set `) and constructs a type from this: `(* -> *) -> *`.

Yes, thanks for the clarification!
Post reply on HN