Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Free-types: Higher kinded types in TypeScript

github.com

Post reply on HN
Print view View original

21–30 of 51 posts

Re: Free-types: Higher kinded types in TypeScript

#21

Post by evolveyourmind »

moomin wrote: post #17
esperent wrote: post #12

I'm reasonably proficient in Typescript although I wouldn't call myself an expert in type systems. But I'm not a beginner either. However, I read though the readme and I have no idea what the usefulness of this is. Can anyone explain, in simple terms, some practical use cases for this?

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 u…

Other than Monads, HKT can be used to easily write type-level functional programs [1]. This can for example help writing type-level parsers for other lanugages.

A real world use-case could be parsing GraphQL raw string queries and automatically infer the returned types based on a common schema, without using special code-generators. For instance you can come up with some magic function `gql_parsed` like:

doc = gql_parsed`query GetUser { user { name }}`

where doc is inferred as something like Doc>

[1] https://desislav.dev/blog/tsfp/

Re: Free-types: Higher kinded types in TypeScript

#22

Post by gizmo »

moomin wrote: post #17
esperent wrote: post #12

I'm reasonably proficient in Typescript although I wouldn't call myself an expert in type systems. But I'm not a beginner either. However, I read though the readme and I have no idea what the usefulness of this is. Can anyone explain, in simple terms, some practical use cases for this?

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 u…

I think there is a certain kind of programmer who enjoys the aesthetics of higher-kinded types, and after having made the investment to truly grok them, wants these HKTs to also be useful in practice.

I don’t think the benefit ever materializes and highly abstract code is just indulgence.

Much like the people who endlessly tinker with their IDE/emacs/desktop environment/shell in the name of productivity.

Re: Free-types: Higher kinded types in TypeScript

#23

Post by ReleaseCandidat »

esperent wrote: post #12

I'm reasonably proficient in Typescript although I wouldn't call myself an expert in type systems. But I'm not a beginner either. However, I read though the readme and I have no idea what the usefulness of this is. Can anyone explain, in simple terms, some practical use cases for this?

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` 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`, `Maybe` (`= T | undefined`), ... HKT give you the possibility to write the type of such type functions.

Re: Free-types: Higher kinded types in TypeScript

#24

Post by ReleaseCandidat »

stevefan1999 wrote: post #6

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.

"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(*) -> *` - read each asterisk as "type". Type constructor that take two types arguments have the kind `* -> * -> *` (Rust-y: `fn(*, *) -> *`). A higher (-order) kinded type takes (for example) a type constructor (here a type constructor which takes just one argument) and generates a type from it: `(* -> *) -> *` (Rust-y: `fn(fn(*) -> *) -> *`.

Edit: I hope now all asterisks are properly escaped ...

Re: Free-types: Higher kinded types in TypeScript

#25

Post by pyrale »

amitport wrote: post #10
davedx wrote: post #2

I’d love to be able to do dependent types in TS. Does this make that possible?

No. Typescript cannot access runtime values (I assume you mean types that depend on runtime values). In TypeScript types can depend on other types and it does support literal types which covers a lot of use cases. What do you need dependent types for? [Edit: why the down vote?]

> 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.

Re: Free-types: Higher kinded types in TypeScript

#26

Post by demurgos »

esperent wrote: post #12

I'm reasonably proficient in Typescript although I wouldn't call myself an expert in type systems. But I'm not a beginner either. However, I read though the readme and I have no idea what the usefulness of this is. Can anyone explain, in simple terms, some practical use cases for this?

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`, and if using `rxjs` it should be `select(selector: string): Observable`. Let's also assume that it has a second method `windowHeight` returning an observable for the window height (`Stream` or `Observable`).

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 {
      select(selector: string): Obs;
      windowHeight(): Obs;
    }
    // The best we can do is type it as `Cycle>` or `Cycle>`.
    
    // With HKTs, using syntax from this lib, you could do:
    interface Cycle {
      select(selector: string): apply;
      windowHeight(): apply;
    }
    // This allows to get the precise signatures we wanted (with the right observable impl, without `unknown`)

Re: Free-types: Higher kinded types in TypeScript

#27

Post by ReleaseCandidat »

ReleaseCandidat wrote: post #24
stevefan1999 wrote: post #6

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.

"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.

Re: Free-types: Higher kinded types in TypeScript

#28

Post by pyrale »

davedx wrote: post #2

I’d love to be able to do dependent types in TS. Does this make that possible?

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.

Re: Free-types: Higher kinded types in TypeScript

#29

Post by ReleaseCandidat »

pyrale wrote: post #28
davedx wrote: post #2

I’d love to be able to do dependent types in TS. Does this make that possible?

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.

For anybody interested in the details, here is the last report of the ongoing implementation of dependent types in GHC: https://discourse.haskell.org/t/ghc-dh-weekly-update-6-2023-...

Re: Free-types: Higher kinded types in TypeScript

#30

Post by amitport »

pyrale wrote: post #25
amitport wrote: post #10

Earlier quoted context omitted.

No. Typescript cannot access runtime values (I assume you mean types that depend on runtime values). In TypeScript types can depend on other types and it does support literal types which covers a lot of use cases. What do you need dependent types for? [Edit: why the down vote?]

> 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 typescript execution phase.

Post reply on HN