RFC avoid combinatorial explosion of overloadings

[gcanti]

This is a follow up of #152 (comment)

The problem

Currently we have to define many overloadings in order to prove to the compiler that a generic HKT can be converted into a concrete type. For example from

HKT<'Option', number>

to

Option<number>

It works pretty well but there is a downside: we get a combinatorial explosion of overloadings.

A possible solution

I've got an idea, what if we can combine the stability of the latest version with the smartness of the previous one?

Here's the plan

1. remove all current overloadings

2. define two type-level dictionaries

// type-level dictionary for HKTs with one type parameter: Option<A>, Task<A>, etc..
export interface URI2HKT<A> {}

export type HKTS = keyof URI2HKT<any> // helper

// type-level dictionary for HKTs with two type parameters: Either<L, A>, etc..
export interface URI2HKT2<L, A> {}

export type HKT2S = keyof URI2HKT2<any, any> // helper

3. for each data structure add an entry in the proper type-level dictionary which maps a URI to its concrete type

Examples

Option

declare module './HKT' {
  interface URI2HKT<A> {
    'Option': Option<A>
  }
}

Either

declare module './HKT' {
  interface URI2HKT2<L, A> {
    'Either': Either<L, A>
  }
}

4. define the minimum number of necessary overloadings in terms of those type-level dictionaries

Example: Functor's lift

export class Ops {
  
  // overloading for all HKT2s (like Either)
  lift<F extends HKT2S, A, B>(F: Functor<F>, f: (a: A) => B): <L>(fa: URI2HKT2<L, A>[F]) => URI2HKT2<L, B>[F]
  
  // overloading for all HKTs (like Option, Task, etc..)
  lift<F extends HKTS, A, B>(F: Functor<F>, f: (a: A) => B): (fa: URI2HKT<A>[F]) => URI2HKT<B>[F]
  
  // base case
  lift<F, A, B>(F: Functor<F>, f: (a: A) => B): (fa: HKT<F, A>) => HKT<F, B>
  lift<F, A, B>(F: Functor<F>, f: (a: A) => B): (fa: HKT<F, A>) => HKT<F, B> {
    return fa => F.map(f, fa)
  }
}

Result: the compiler does the heavy lifting

import * as option from 'fp-ts/lib/Option'
import * as either from 'fp-ts/lib/Either'
import { lift } from 'fp-ts/lib/Functor'

const double = (n: number) => n * 2

// liftedOptionDouble: (fa: option.Option<number>) => option.Option<number>
export const liftedOptionDouble = lift(option, double)

// liftedEitherDouble: <L>(fa: either.Either<L, number>) => either.Either<L, number>
export const liftedEitherDouble = lift(either, double)

What do you think?

(I'm writing a POC on a branch so we can reason on actual code, I'll post a link asap)

[SimonMeskens]

I've been working on my liftFantasy all morning and it basically boiled down to solving this issue. I managed to fix it in a number of different ways. One really clever way was using typelevel-ts' ObjectOverwrite to overwrite _A in a concrete version of a HKT. This works, but it breaks on any types with symbol keys, because you can't copy over symbol properties with typelevel-ts (keyof only returns string keys).

All of the solutions I found have issues and the only one that reliably works is the dictionary you propose. So I'm in favor of this. One issue with the dictionary versus the current "proofs" is that it's less type-safe. The proofs are guaranteed by the compiler to be correct, the dictionary isn't.

I could add "array": Option<A> to the dictionary and that would produce code that only breaks at runtime. The solution would be to have a constraint on A. I'll work on providing the code for a constrained dictionary, I think it might be possible, but it's a little more complex. I'll get back to you in a few.

[gcanti]

One issue with the dictionary versus the current "proofs" is that it's less type-safe. The proofs are guaranteed by the compiler to be correct, the dictionary isn't

This is worrisome, could you please elaborate on this? IMO this proposal would improve the type safety: currently there are tons of overloadings and each of them is a POU (point of unsafety :) ). Now when I define a new data structure I must write many overloadings therefore the probability of writing a wrong one is high.

These dictionaries would allow to keep the majority of overloadings within the library reducing the work in userland

Or are you referring to this kind of proofs?

fp-ts/src/Option.ts

Line 293 in 92bc1ed

export const option: Monad<URI> &

[SimonMeskens]

This is worrisome, could you please elaborate on this?

The proofs I was referring to were the POUs. I just noticed that the compiler indeed lets you write false ones, so they're less safe than I thought.

The unsafety I refer to is when you put an incorrect entry in the dictionary, like 'array': Option<A>, but I just looked into it and it doesn't seem like I can fix that. In any case, you are correct that the dictionary solution is way more type-safe than the current method :)

I love it :)

[gcanti]

'array': Option

yeah, would be a disaster, though I guess you would spot the error pretty quickly as soon as you try to use your new data structure. I'm more concerned by the number of the overloadings still present within the library and which are basically dangerous unsafeCoerce. However I can't think of a solution that would reduce further their number

[SimonMeskens]

I managed to make the compiler complain about it!

export interface URI2HKT<A> {
    'Array': Option<A>;
}

export type HKTS = keyof URI2HKT<any>;

type HKTTest<U, A, B extends HKT<U, A>> = B;
type HKTof<U extends HKTS, A> = HKTTest<U, A, URI2HKT<A>[U]>;

URI2HKT<A>[F], would also be equal to HKTof<F, A>, so you can use whichever in your code.

EDIT: dammit, it doesn't quite work, I'm close though

[SimonMeskens]

The code above does seem to work, but requires me to edit a bunch of stuff all over the library, I'm going to check out the library itself and try it out. The way it works is that HKTTest is only valid when URI2HKT[U] is actually a HKT<U, A>>

EDIT: I think it's either a bug or a limitation of TypeScript

[gcanti]

Here's the POC #155

[SimonMeskens]

I figured out a way better fix, I'll commit it to the POC branch

compliments to @NaridaL for the help

[gcnew]

Is the purpose of

type HKTTest<U, A, B extends HKT<U, A>> = B;

to make sure that you can't accidentally write

interface URI2HKT<A> {
    'Array': Option<A>;
}

If that's its purpose, wouldn't the following be enough? I haven't tried it with multiple files, though.

const HKTS_check: { [k in keyof URI2HKT<any>]: HKT<k, any> } = null! as URI2HKT<any>;
// Type 'Option<any>' is not assignable to type 'HKT<"Array", any>'.
//   Types of property '_URI' are incompatible.
//     Type '"Option"' is not assignable to type '"Array"'.

[SimonMeskens]

@gcnew Have a look at the POC branch, I found a super simple solution, it's causing weird bugs with vscode though, and I can't seem to figure out why. Seems like the compiler is having a hissy fit or something.

[gcnew]

@SimonMeskens Do you mean the errors mentioned in #155?

[SimonMeskens]

Yeah, that HKTS_check solution seems to fix it though, I'll commit that

[gcnew]

It's basically the same fix; the only difference being that my check is on the expression level. Unfortunately the (better) type level solution is circular and the compiler complains :/.

[SimonMeskens]

This one works:

export type HKTMap<T extends string> = { [K in T]: HKT<K, any> }

export interface URI2HKT<A> extends HKTMap<HKTS> {}

export type HKTS = keyof URI2HKT<any>

But that's the one that's causing strange ghost bugs in the compiler. You can run the compiler twice on different hardware and get different results. I assume it's a file ordering thing.

[SimonMeskens]

I'm worried that any attempt to typecheck the map will run into file ordering issues eventually.

[gcnew]

A stupid work-around may be every file that augments URI2HKT to have a separate HKTS_check.

[SimonMeskens]

yeah, that's cognitive load you really can't push onto the user

[SimonMeskens]

The map checker already discovered two bugs though, so it's clearly a useful thing, maybe we should just move it into a test instead, as that's basically what it's doing. That would mean you can still have bugs with the map in userland though. The user could then also put the check in his test suite I guess?

[gcnew]

It's ugly but I guess it's better than nothing. The good thing is that if one wants to add new HKTs, chances are they know what they are doing and this will provide them with some basic checking against human errors.

[SimonMeskens]

This one passes the Travis, so I guess we'll leave it in for now, thanks for the solution. @NaridaL already showed me a similar solution, but then we stumbled onto the other one that was more elegant.

[SimonMeskens]

Do note that the current solution will be stripped away by the compiler, so it doesn't work in userland.

[SimonMeskens]

@gcanti @gcnew I constructed a new type that does integrity checking. The way it works is that we'd use this type instead of URI2HKT[U] in the interfaces and if you try to give it a type that's not sound, it returns never.

The trick is [key in URI2HKT<A>[URI]['_URI']]. It returns only types where _URI matches its lookup.

I'm not going to commit this yet, as I think I can still improve further on the system and move the check onto the map itself. It's hard to write though, as I ran into the weirdest bug: microsoft/TypeScript#17238

What do you guys think?

// type-level integrity-checking types. HKTAs<U, A> is the same as URI2HKT<A>[U],
// but HKTAs<U, A> returns type `never` for types that have incorrect URI mappings

export type HKTAs<URI extends HKTS, A> = (
  {[key in URI2HKT<A>[URI]['_URI']]: URI2HKT<A>[URI]} &
  { [key: string]: never }
)[URI]

export type HKT2As<URI extends HKT2S, L, A> = (
  {[key in URI2HKT2<L, A>[URI]['_URI']]: URI2HKT2<L, A>[URI]} &
  { [key: string]: never }
)[URI]

[gcanti]

The way it works is that we'd use this type instead of URI2HKT[U] in the interfaces and if you try to give it a type that's not sound, it returns never

@SimonMeskens what do you mean with "in the interfaces"? What kind of interfaces?

[SimonMeskens]

@gcanti For example, Functor:

export interface Functor<F extends HKTS> {
  readonly URI: F
  map<A, B>(f: (a: A) => B, fa: HKTAs<F, A>): HKTAs<F, B>
}

I found a better implementation too, moving the check into HKTS, which means you never get the never type. It also supports 2 parameter HKTs implementing one parameter interfaces, which is currently an open issue (for example, if we correctly type the Functor interface, Either can't implement it, as it's not in URI2HKT.

Here's the updated HKT.ts. I think this version is a lot better than what we have now:

export interface HKT<URI extends HKTS, A> {
  readonly _URI: URI
  readonly _A: A
}

export interface HKT2<URI extends HKT2S, L, A> extends HKT<URI, A> {
  readonly _L: L
}

// type-level dictionaries for HKTs

export interface URI2HKT<A> {}
export interface URI2HKT2<L, A> {}

// URI constrains with dictionary integrity check

export type HKTS = HKT2S | keyof {
  [key in URI2HKT<any>[keyof URI2HKT<any>]['_URI']]: any
}

export type HKT2S = keyof {
  [key in URI2HKT2<any, any>[keyof URI2HKT2<any, any>]['_URI']]: any
}

// HKTAs<U, A> is the same as URI2HKT<A>[U], but checks for URI constraints

export type HKTAs<URI extends HKTS, A> = (URI2HKT<A> & URI2HKT2<any, A>)[URI]

export type HKT2As<URI extends HKT2S, L, A> = URI2HKT2<L, A>[URI]

[SimonMeskens]

I edited the above post a little (mainly just commented better). I personally feel like this is probably the best version we can get. It's completely typesafe and has the same cognitive load as the current released version (forcing userland to use indexers with URI2HKT[URI] felt a bit iffy anyway).

[SimonMeskens]

I found one very tiny edge case, the integrity check only checks if the key/type is correct through checking the _URI type, but it doesn't check if the type actually contains _URI, _A or _L. I'm sure I can figure out a way to do that. I'll work on it, but it's such a rare edge case that it probably doesn't matter that much (still, it's a library, less footguns is a good thing).

[gcanti]

@SimonMeskens You are doing a terrific job but I'm worried about touching the core which I would like to keep as simple as possible (also I'm worried about hitting a compiler bug)

Indeed this proposal is only related to improve the transformation from a generic HKT<URI, A> to the corresponding concrete type which can be done

• manually (example cast from HKT<'Option', number> to Option<number>)
• with specific overloadings (current implementation)
• with global type level dictionaries (this proposal)

Also I would like to be able to swap these solutions without touching the core.

Now for what concerns type level checks, the current solution

/* tslint:disable */
(null! as URI2HKT<any>) as { [k in keyof URI2HKT<any>]: HKT<k, any> }
(null! as URI2HKT2<any, any>) as { [k in keyof URI2HKT2<any, any>]: HKT2<k, any, any> }
/* tslint:enable */

while not perfect (will be erased by the compiler) is cheap, effective:

• detects wrong URIs
• dtetects wrong HKT/HKT2 phantom types

and not intrusive (no changes in the codebase)

[SimonMeskens]

I think I disagree, but I understand your point. It's easily possible to make a non-intrusive version, however:

export interface HKT<URI, A> {
  readonly _URI: URI
  readonly _A: A
}

export interface HKT2<URI, L, A> extends HKT<URI, A> {
  readonly _L: L
}

// type-level dictionaries for HKTs

export interface URI2HKT<A> {}
export interface URI2HKT2<L, A> {}

// URI constrains with dictionary integrity check

export type HKTS = keyof {
  [key in URI2HKT<any>[keyof URI2HKT<any>]['_URI']]: any
}

export type HKT2S = keyof {
  [key in URI2HKT2<any, any>[keyof URI2HKT2<any, any>]['_URI']]: any
}

// HKTAs<U, A> is the same as URI2HKT<A>[U], but checks for URI constraints

export type HKTAs<URI extends HKTS, A> = URI2HKT<A>[URI]

export type HKT2As<URI extends HKT2S, L, A> = URI2HKT2<L, A>[URI]

This version will not change anything to the codebase, but still offers the use of a typesafe version of URI2HKT. Wherever you would write URI2HKT[U], you write instead HKTAs<U, A>. Instead of a large change, it's just a better version of URI2HKT. How does that sound?

[SimonMeskens]

This version shouldn't come anywhere near a compiler bug btw. All the compiler bugs are related to generic indexation, something which this version is not using.

[gcanti]

With core I mean the base interfaces implementing type classes, based on this comment #153 (comment), I thought you have to touch them. However if you are only talking about the URI2HKT implementation I'm definitely open to better alternatives, so please put up a POC, maybe by forking the current working branch #155

[SimonMeskens]

Good idea, I'll fork the repo onto my Github (to keep this repo clean) and fork the #155 branch to make a POC with the above and make a PR so you can look it over. I'll do this hopefully tomorrow (today is a bit busy)

[gcanti]

FWIW if the goal is checking that the map URI -> <concrete-type>['_URI'] is consistent, the following should work without changing the current POC and it will survive to the compilation step

//
// extracted from typelevel-ts
//

export type Bool = 'true' | 'false'

export type And<B1 extends Bool, B2 extends Bool> = {
  false: 'false'
  true: {
    false: 'false'
    true: 'true'
  }[B2]
}[B1]

export type StringContains<S extends string, L extends string> = ({ [K in S]: 'true' } & {
  [key: string]: 'false'
})[L]

export type StringEq<L1 extends string, L2 extends string> = And<StringContains<L1, L2>, StringContains<L2, L1>>

//
// typecheck URI -> <concrete-type>['_URI']
//

// map HKT's URI -> is valid
export type AreHKTValid = { [K in HKTS]: StringEq<K, URI2HKT<any>[K]['_URI']> }

// proof that AreHKTValid is a map string -> 'true'
export interface Proof extends AreHKTValid {
  [key: string]: 'true'
}

// map HKT2's URI -> is valid
export type AreHKT2Valid = { [K in HKT2S]: StringEq<K, URI2HKT2<any, any>[K]['_URI']> }

// proof that AreHKT2Valid is a map string -> 'true'
export interface Proof2 extends AreHKT2Valid {
  [key: string]: 'true'
}

Bonus point: hovering on the AreHKTValid type, you can spot the offending definition

---

I think it doesn't worth it though, since

(null! as URI2HKT<any>) as { [k in keyof URI2HKT<any>]: HKT<k, any> }
(null! as URI2HKT2<any, any>) as { [k in keyof URI2HKT2<any, any>]: HKT2<k, any, any> }

gives me much more with much less. I'm with @gcnew on this

The good thing is that if one wants to add new HKTs, chances are they know what they are doing and this will provide them with some basic checking against human errors

Once we know how to do it, we could just document the best practices for writing new data structures

[SimonMeskens]

Yeah, I didn't quite understand the intention of the library, now that I do, it makes total sense. I agree with your post too, if the intention is just to do a very quick integrity check, that small 2-liner is perfect. It's probably a good thing that it compiles away actually, as it would provide the user with a very cryptic error in the library, instead of at the location where the mistake is made. I've looked for a solution that gives an error in the correct file, but it doesn't seem possible.

I still think there's merit to moving the check into HKTS though and just make sure you can't get an invalid type out of the dictionary. I'm currently finishing up the POC branch, so I can show what I mean.

[SimonMeskens]

POC in #158

[gcanti]

Released in fp-ts@next

[gcanti]

I checked 0.4.1 against

• io-ts
• monocle-ts
• parser-ts
• graphics-ts
• fractal-trees-ts
• fp-ts-rxjs

@SimonMeskens There's a problem with HKTS / HKT2S

type HKTS = URI2HKT<any>[keyof URI2HKT<any>]['_URI']; // errors: Type 'never' cannot be used as an index type
type HKT2S = URI2HKT2<any, any>[keyof URI2HKT2<any, any>]['_URI']; // error: Type 'never' cannot be used as an index type

In particular keyof URI2HKT<any> and keyof URI2HKT2<any, any> are both never when URI2HKT and URI2HKT2 are empty

Here's a repro https://github.com/gcanti/fp-ts-rxjs (branch latest), npm run build is broken

A possible fix is switching back to previous definitions

HKTS = keyof URI2HKT<any>
HKT2S = keyof URI2HKT2<any, any>

[SimonMeskens]

It's odd that the compiler thinks it's empty. Let me see if there's a simple fix that still does the same thing. I already have one in mind. I didn't realize it would type keyof as never if there are no keys, I assumed it would then pick string instead.

[SimonMeskens]

Simplest fix (I really like this one):

type HKTS = (URI2HKT<any> & { never: HKT<never, never> })[keyof URI2HKT<any> | 'never']['_URI']
type HKTS2 = (URI2HKT2<any, any> & { never: HKT<never, never> })[keyof URI2HKT2<any, any> | 'never']['_URI']

Simply adds a bottom type to HKTS

[gcanti]

Great, let me check against the list above

[gcanti]

Works like a charm, would you like to send a PR?

[SimonMeskens]

Sure, coming up

[gcanti]

@SimonMeskens Released a patch in fp-ts@next (0.4.2)