KiaraGrouwstra / typical

playground for type-level primitives in TypeScript
MIT License
173 stars 5 forks source link

Typesafe dates #7

Closed atennapel closed 6 years ago

atennapel commented 6 years ago

A way to encode dates on the typelevel is something like this:

type Month = '1' | '2' | '3' | '4' | '5' | '6' | '7' | '8' | '9' | '10' | '11' | '12';
type Day<M extends Month> = {
    1: '1' | '2' | '3' | '4' | '5' | '6' | '7' | '8' | '9' | '10' | '11' | '12' | '13' | '14' | '15' | '16' | '17' | '18' | '19' | '20' | '21' | '22' | '23' | '24' | '25' | '26' | '27' | '28' | '29' | '30' | '31',
    2: '1' | '2' | '3' | '4' | '5' | '6' | '7' | '8' | '9' | '10' | '11' | '12' | '13' | '14' | '15' | '16' | '17' | '18' | '19' | '20' | '21' | '22' | '23' | '24' | '25' | '26' | '27' | '28' | '29',
    3: '1' | '2' | '3' | '4' | '5' | '6' | '7' | '8' | '9' | '10' | '11' | '12' | '13' | '14' | '15' | '16' | '17' | '18' | '19' | '20' | '21' | '22' | '23' | '24' | '25' | '26' | '27' | '28' | '29' | '30' | '31',
    4: '1' | '2' | '3' | '4' | '5' | '6' | '7' | '8' | '9' | '10' | '11' | '12' | '13' | '14' | '15' | '16' | '17' | '18' | '19' | '20' | '21' | '22' | '23' | '24' | '25' | '26' | '27' | '28' | '29' | '30',
    5: '1' | '2' | '3' | '4' | '5' | '6' | '7' | '8' | '9' | '10' | '11' | '12' | '13' | '14' | '15' | '16' | '17' | '18' | '19' | '20' | '21' | '22' | '23' | '24' | '25' | '26' | '27' | '28' | '29' | '30' | '31',
    6: '1' | '2' | '3' | '4' | '5' | '6' | '7' | '8' | '9' | '10' | '11' | '12' | '13' | '14' | '15' | '16' | '17' | '18' | '19' | '20' | '21' | '22' | '23' | '24' | '25' | '26' | '27' | '28' | '29' | '30',
    7: '1' | '2' | '3' | '4' | '5' | '6' | '7' | '8' | '9' | '10' | '11' | '12' | '13' | '14' | '15' | '16' | '17' | '18' | '19' | '20' | '21' | '22' | '23' | '24' | '25' | '26' | '27' | '28' | '29' | '30' | '31',
    8: '1' | '2' | '3' | '4' | '5' | '6' | '7' | '8' | '9' | '10' | '11' | '12' | '13' | '14' | '15' | '16' | '17' | '18' | '19' | '20' | '21' | '22' | '23' | '24' | '25' | '26' | '27' | '28' | '29' | '30' | '31',
    9: '1' | '2' | '3' | '4' | '5' | '6' | '7' | '8' | '9' | '10' | '11' | '12' | '13' | '14' | '15' | '16' | '17' | '18' | '19' | '20' | '21' | '22' | '23' | '24' | '25' | '26' | '27' | '28' | '29' | '30',
    10: '1' | '2' | '3' | '4' | '5' | '6' | '7' | '8' | '9' | '10' | '11' | '12' | '13' | '14' | '15' | '16' | '17' | '18' | '19' | '20' | '21' | '22' | '23' | '24' | '25' | '26' | '27' | '28' | '29' | '30' | '31',
    11: '1' | '2' | '3' | '4' | '5' | '6' | '7' | '8' | '9' | '10' | '11' | '12' | '13' | '14' | '15' | '16' | '17' | '18' | '19' | '20' | '21' | '22' | '23' | '24' | '25' | '26' | '27' | '28' | '29' | '30',
    12: '1' | '2' | '3' | '4' | '5' | '6' | '7' | '8' | '9' | '10' | '11' | '12' | '13' | '14' | '15' | '16' | '17' | '18' | '19' | '20' | '21' | '22' | '23' | '24' | '25' | '26' | '27' | '28' | '29' | '30' | '31'
}[M]

type MyDate<M extends Month, D extends Day<M>> = { month: M, day: D };

function date<M extends Month, D extends Day<M>>(month: M, day: D): MyDate<M, D> {
  return { month, day };
}

const date1 = date('1', '31'); // typechecks
const date2 = date('2', '31'); // fails

Do you know a way to do this more concisely or with numbers instead of strings?

KiaraGrouwstra commented 6 years ago

Cool idea. :)

with numbers

So, removing the quotes and optionally turning the object into a tuple yields this error:

Type 'M' cannot be used to index type ...

Month is in fact guaranteed to satisfy the index requirement though, so this qualifies as a bug. Feel free to mention the related https://github.com/Microsoft/TypeScript/issues/13514. There may be a few more related issues.

more concisely

type To29 = '1' | '2' | '3' | '4' | '5' | '6' | '7' | '8' | '9' | '10' | '11' | '12' | '13' | '14' | '15' | '16' | '17' | '18' | '19' | '20' | '21' | '22' | '23' | '24' | '25' | '26' | '27' | '28' | '29';
type To30 = To29 | '30';
type To31 = To30 | '31';
type Day<M extends Month> = { 1: To31, 2: To29, 3: To31, 4: To30, 5: To31, 6: To30, 7: To31, 8: To31, 9: To30, 10: To31, 11: To30, 12: To31 }[M];

Edit: It'd be cool to get the type level on par with the run-time level so we could e.g. do the built-in functions on the type level as well. the bottle-neck there is the current lack of type level arithmetic operators though. The TS team doesn't want them though (ref); I looked into it but figured it'd take a bit of effort to put them in as well.

atennapel commented 6 years ago

Hey thanks for the reply! Yeah it would be awesome to have some form of dependent types in Typescript, similar to the DOT calculus does for Scala. Being able to run functions at compile-time would be amazing too. This could probably be done with a pre-processor similar to Template Haskell and would probably be pretty easy to implement for pure functions where the arguments are known at compile-time.

KiaraGrouwstra commented 6 years ago

Being able to run functions at compile-time would be amazing too.

Running functions at compile-time sounds like executing user JS rather than calculating types. I have tried something related though, calculating the return types of functions at the type level (to use in other types), see https://github.com/Microsoft/TypeScript/pull/17961. I hadn't managed to finish it yet though.

Yeah it would be awesome to have some form of dependent types in Typescript, similar to the DOT calculus does for Scala.

I'd checked a book on DOT with Idris for ideas in that area and how they might apply here. I think the textbook example of fixed-length vectors has been possible already. One of the more interesting things they were doing though was type constraints such as to create type-safe division, with a custom user constraint to e.g. disallow 0. That's something else I was exploring in that PR 17961, though still a experimental WIP as well.

atennapel commented 6 years ago

Do you know if there's a way at the moment to type a function similar to this:

function f(x: number | string) {
  return typeof x === 'string'? +x: '' + x;
}

I'd like the return type to depend on the input type, something like Haskell's type families would do the trick I think:

type F<number> = string;
type F<string> = number;

function f<T extends number | string>(x: T): F<T> {
  return typeof x === 'string'? +x: '' + x;
}

I am not that experienced yet in TypeScript so maybe this can already be done in some way?

EDIT: Sadly this doesn't seem to work:

interface F {
  (x: number): string;
  (x: string): number;
}

const f: F = (x: number | string) => typeof x === 'string'? +x: '' + x;
KiaraGrouwstra commented 6 years ago

It seems in your example inference is getting confused by the ternary operator. Technically it should be following that using a type guard. See one related(-ish?) issue here. It actually sounds like you might be able to just open a new issue over at TS for that.

Full-fledged type-level type checks aren't possible yet (in my PR above I wanted to do that by hooking into e.g. the interface you showed there). That being said, for this easier case concerning simple types, there has been a hack involving writing stuff to the global class types as demonstrated e.g. here, the reasoning being that we can do checks on string literal types, even though we cannot do checks on types in a more general fashion.

atennapel commented 6 years ago

I had another question/puzzle for you. I have the following piece of code (attempt at type-safe Redux):

// my actions
type Actions = {
    INC: number,
    DEC: number,
    DISPLAY: string,
}

// boilerplate
type Types = keyof Actions;
type Action<T extends Types> = { type: T, val: Actions[T] }
type ActionVal<T extends Types, A extends Action<T>> = A['val'];
type ActionC<T extends Types> = (val: T) => Action<T>
type ReducerMap<S> = {[k in keyof Actions]: (state: S, val: Actions[k]) => S }
const reducer = <S>(map: ReducerMap<S>) => (state: S, action: Action<Types>): S => 
    (map[action.type] as any)(state, action.val) as S;

// my reducer
type State = number;

const myReducer = reducer<State>({
    INC: (state, n) => state + n,
    DEC: (state, n) => state + n,
    DISPLAY: (state, str) => {
        console.log(str);
        return state;
    },
});

I got it almost working except for the use of any. If I remove the any I get:

Cannot invoke an expression whose type lacks a call signature. Type '((state: S, val: number) => S) | ((state: S, val: number) => S) | ((state: S, val: string) => S)' has no compatible call signatures.

Do you know of any way to fix this?

Another problem is that the types depend on the very specific Actions while I would like it to be any Actions object given by the users. I don't think this is solvable though...

KiaraGrouwstra commented 6 years ago

action is a union (it can't know which here yet), which propagates to action.val, as a result of which the parameters don't match any of the (unioned) function signatures. Yeah, it's pretty tough, don't see an elegant solution here off the top off my head.

KiaraGrouwstra commented 6 years ago

I hope the original question is resolved here, then I'll mark as closed. I care about typed Redux as well, because proper typing could help solve the boilerplate there that is making front-end unbearable. I think TS is still missing a few pieces of the puzzle, and I'm interested in further exploring Flow to that end as well. I'll track that in a separate issue.