7 ms·

Free-types: Higher kinded types in TypeScript

• davedx 3y ago
  I’d love to be able to do dependent types in TS. Does this make that possible?
  • frogulis 3y ago
    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.
    • pxeger1 3y ago
      Typescript's type system is already undecidable (except that they limit recursion depth). I don't know much about dependent types but I'd guess it similarly doesn't matter much in practice that in the general case they're undecidable?
    • Smaug123 3y ago
      A fully-featured dependent type system may be undecidable, but that doesn't mean you can't make one - it just means that there will be valid programs that the type checker nevertheless rejects, or there will be valid programs for which the type checker never terminates. It doesn't stop you from creating a type checker in the first place; it just weakens the guarantees you can make about that type checker. The Typescript type checker is (or at least was) already Turing-complete (https://github.com/microsoft/TypeScript/issues/14833 https://github.com/microsoft/TypeScript/issues/14833) without fully supporting dependent types.
  • amitport 3y ago
    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?]
    • deleted 3y ago
      [deleted]
    • pyrale 3y ago
      > 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.
      • amitport 3y ago
        "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 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.
        • ReleaseCandidat 3y ago
          > The value does not exist during compilation. type Z = []["length"] type One = [0]["length"] type Two = [0,0]["length"]
        • PhilipRoman 3y ago
          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.
          • reuben364 3y ago
            You still need a way of normalizing expressions that is consistent with your runtime. To say that types ((x: bool) => F<true && x>) and ((x: bool) => F<false || x>) are the same, wrt judgemental equality, requires normalizing both to ((x: bool) => F<x>).
  • pyrale 3y ago
    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.
    • ReleaseCandidat 3y ago
      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-06-07/6383 https://discourse.haskell.org/t/ghc-dh-weekly-update-6-2023-...
• epolanski 3y ago
  I wonder how this differs from HKT's implementation in fp-ts 2 and Effect-TS. https://gcanti.github.io/fp-ts/modules/HKT.ts.html https://gcanti.github.io/fp-ts/modules/HKT.ts.html
• noobdev9000 3y ago
  Why
  • mbwgh 3y ago
    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
    • ivxvm 3y ago
      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<T> and MapFunctor<T> to make this useful.
      • mbwgh 3y ago
        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.
        • ivxvm 3y ago
          Oh, so it's just a type alias for readability. Then it makes sense.
    • 3y ago
• stevefan1999 3y ago
  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.
  • DougBTX 3y ago
    For Rust, pre-GAT, there was no way to “output” a type which could be “called” with further arguments (very fuzzy terminology, sorry, best I can do!) or maybe in other words, you could write functions which retuned values, but not new functions. Nowadays, GATs support a bigger subset of HKTs, but still not everything as I understand it. https://blog.rust-lang.org/2022/10/28/gats-stabilization.html https://blog.rust-lang.org/2022/10/28/gats-stabilization.htm...
  • pdpi 3y ago
    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<T> 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 as an input. A higher-kinded type is a higher-order type function. As a concrete example, consider this pseudo-Java method: List<B> map<A,B>(Function<A,B> fn, List<A> as) { ... } You take a list, and you return a list. Thing is, Java has several list implementations: LinkedList, ArrayList, CopyOnWriteArrayList, and a few others. What I'd like to express is that whatever concrete list type goes in is also the concrete type that comes out. If java allowed it, you could express it like this: L<B> map<L<T> extends List<T>,A,B>(Function<A,B> fn, L<A> as) { ... } This map is generic on L, A, and B, but also L is itself generic, so map is "twice-generic", if you will.
    • classified 3y ago
      Finally an explanation that makes sense. Thank you :)
• ToJans 3y ago
  Looking forward to a proper monad lib in Typescript! However, I can only assume that molding/abusing types like this might have a big - if not huge - impact on compilation times... I've created a template-like generic type that allows you compose multiple kinds and replace any property of an object with a function returning the same type as the property, and vscode has such a hard time inferring types that intellisense has become unusable in this context. Curious to see how this will turn out.
  • arnejenssen 3y ago
    I'm using fp-ts https://gcanti.github.io/fp-ts/ https://gcanti.github.io/fp-ts/
    • ToJans 3y ago
      Great tip; thank you!
    • douglasisshiny 3y ago
      fp-ts is great and still has active development but it has also been folded into effect-ts (https://github.com/Effect-TS/ https://github.com/Effect-TS/) which is based on Scala ZIO. I think long-term it will have a larger ecosystem, more active development and a better DX. The docs are far from complete, but give a good intro (https://effect.website/docs/getting-started https://effect.website/docs/getting-started). I'm not associated with effect-ts at all.
• esperent 3y ago
  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?
  • moomin 3y ago
    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.
    • evolveyourmind 3y ago
      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<Query<{GetUser:{user:{name:string}}}>> [1] https://desislav.dev/blog/tsfp/ https://desislav.dev/blog/tsfp/
    • gizmo 3y ago
      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.
      • foderking 3y ago
• xupybd 3y ago
  Are these like type classes?
  • xmcqdpt2 3y ago
    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.
    • ReleaseCandidat 3y ago
      > An HKT is the type of a type constructor. That is a ("normal") kind `* -> *`. A Java `List<_>` or `Set<T>` 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: `(* -> *) -> *`.
• classified 3y ago
  I can't make sense of the examples. What would I use this for?
• jdonaldson 3y ago
  Higher kinded types always remind me of regex. People think “I know, I’ll use HKT to solve this problem”. Now they have two problems. These techniques can be way overkill for someone until they are dealing with an overwhelming amount of types to unify. It’ll seem like a terrible idea until that obstacle is encountered.