A situation where I needed this were typings for Cycle.js a couple years ago. At this time, you could configure it to use the observable library of your choice but it was hard to type. In particular the observable could be a `Stream from "xstream"` or `Observable from "rxjs"`

This lib has a method `select` to return an observable list of DOM elements for a given CSS selector. What should be its signature? If using `xstream`, it should be `select(selector: string): Stream<HTMLElement[]>`, and if using `rxjs` it should be `select(selector: string): Observable<HTMLElement[]>`. Let's also assume that it has a second method `windowHeight` returning an observable for the window height (`Stream<number>` or `Observable<number>`).

We can make the lib object generic over the observable implementation, but you need HKTs to type it properly. The reason is that the lib is generic over an already generic type.

Here is an example:

    // Without HKT (regular generic)
    // Problem: both `select` and `windowHeight` return the same type (we lose the HTMLElement[]/number information)
    interface Cycle<Obs> {
      select(selector: string): Obs;
      windowHeight(): Obs;
    }
    // The best we can do is type it as `Cycle<Stream<unknown>>` or `Cycle<rxjs.Observable<unknown>>`.
    
    // With HKTs, using syntax from this lib, you could do:
    interface Cycle<$HktObs> {
      select(selector: string): apply<$HktObs, HTMLElement[]>;
      windowHeight(): apply<$HktObs, number>;
    }
    // This allows to get the precise signatures we wanted (with the right observable impl, without `unknown`)

Higher (-order) kinded types describe functions on type constructors. Type constructors are "generic types", like `T[]` that generate a list from a single type `T` or like `Map<S, T>` that generates a new type from two types `S` and `T`. A higher kinded type constructor is one, where you could use any (well, with certain prerequisites) of these type constructors to generate a new type. Let's say you want to have a function `map` (like `Array.map`) that works not only with `T[]` but also with `Tree<T>`, `Maybe<T>` (`= T | undefined`), ... HKT give you the possibility to write the type of such type functions.

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.

There’s a couple of ways to think about it: it gives you a way to talk about List rather than List of T, it enables you to write partial types like partially-applied functions, or it makes it possible to define Monads.

But as I say, none of these things will sound immediately useful unless you have experience of using those concepts already.

A simple example I could recall from the other day is something like this:

  export type LinkedWorksheetsRecord = Record<WorksheetId, Record<WorksheetId, ReferenceTypeId[]>>;
  export type LinkedWorksheetsMap = Map<WorksheetId, Map<WorksheetId, ReferenceTypeId[]>>;

What I would rather have written instead is however something like this:

  export type LinkedWorksheets<T> = T<WorksheetId, T<WorksheetId, ReferenceTypeId[]>>;
  ...
  const myMap: LinkedWorksheets<Map> = ...;

This is however not possible, because `Map` is a type constructor which expects two more type arguments `K, V` until it is a fully applied, concrete type `Map<K, V>`.

With a library like this, this is probably possible (unless I've missed something which wouldn't surprise me). It would unfortunately surely be more verbose.

Still, I would be against pulling in a dependency only for something like this. The above example is simple I believe, but not exactly a "killer-app". And no, Monads aren't either (if you don't limit effects and don't have do-notation) :P

I'm using fp-ts https://gcanti.github.io/fp-ts/

Might be wrong here, but I'm of the understanding that a dependent type system is undecidable, and so to have static dependent types you need to have a more restricted language, like the inability to write arbitrarily recursive functions.

In short I don't think so but I'd also love a good explanation as to why I'm wrong.

I guess you could use it to implement an algebra that allows you to build dependent types, but that would be unfit for practical uses.

As a case in point, Haskell has first-class experience for HKTs, and dependent types implementation in haskell is getting hindered by the limits of the language.

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<B> map(C<A> coll, Function<A, B> 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> {
      C<B> map(C<A> coll, Function<A,B> 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<B> foo(Mappable<C> inst, C<A> 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<B> foo(Mappable<C> inst, C<A> coll) {
      var out = 0;
      inst.map(coll, k -> {out++; return k});
      return out;
    }

So that function would be enough to prove that Mappable<C> 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.

Finally an explanation that makes sense. Thank you :)

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.