Trying to implement Logic using the the type-system

[damodharanj]

type Bool = 'true' | 'false'

type Or<A extends Bool, B extends Bool> = A extends 'true' ? 'true' : B;

type And<A extends Bool, B extends Bool> = A extends 'true' ? B extends 'true' ? 'true' : 'false' : 'false';

type Not<T extends Bool> = T extends 'true' ? 'false' : 'true';

type Test = Not<'true'>

type Test1 = Not<'false'>

type Test3 = Not<Or<'true', 'false'>>

type Test4 = And<Not<'true'>, Not<'false'>>

function test(a: Bool): Not <typeof a> {
    switch (a) {
        case 'false': return 'false';
        case 'true': return 'true';
    }
}

The test function is supposed to return 'true' for input 'false' and vice-versa. But I don't get a error for the above implementation.

[DanielRosenwasser]

2 problems:

1. typeof a is always Bool, and Not<Bool> simplifies to Bool. If you want to make it dependent on the type that will eventually be given in place of a, you have to make the signature generic like so: function test<T extends Bool>(a: T): Not <T>
2. There's no way to implement conditional types today, so once you've done that you'll need a cast.

In the future

1. please format your code snippets using code fences using three backticks:

```ts
// Sample code goes here.
```

2. Ask "how do I do this?" questions in StackOverflow, or have your issues follow the template we provide.

[damodharanj]

type Bool = 'true' | 'false'

type Or<A extends Bool, B extends Bool> = A extends 'true' ? 'true' : B;

type And<A extends Bool, B extends Bool> = A extends 'true' ? B extends 'true' ? 'true' : 'false' : 'false';

type Not<T extends Bool> = T extends 'true' ? 'false' : 'true';

type Test = Not<'true'>

type Test1 = Not<'false'>

type Test3 = Not<Or<'true', 'false'>>

type Test4 = And<Not<'true'>, Not<'false'>>

function test<T extends Bool>(a: T): Not<T> {
  switch (a) {
    case 'false':
      return "true" as Not<T>;
    case 'true':
      return 'false' as Not<T>;
    default:
      return 'true' as Not<T>;
  }
}

The fix works only with assertion as well as default handling. Since typescript has dependent types was trying out the theorem prover like features.

[rubenpieters]

Related to #33014 and #30284 . In the prototype implementation of the former ( #33237 ), which is restricted to working with indexed access types for now, the following adapted example works as you expect (both in positive and negative cases):

type Bool = "true" | "false"

type Not = {
    "true": "false",
    "false": "true",
}

function f1<T extends Bool>(a: T): Not[T] {
    if (a === "false") {
        // no error
        return "true";
    } else {
        // no error
        return "false";
    }
}

function f2<T extends Bool>(a: T): Not[T] {
    if (a === "false") {
        // error
        return "false";
    } else {
        // error
        return "true";
    }
}

Also for a different formulation of And:

type And = {
  "true": {
    "true": "true",
    "false": "false",
  },
  "false": {
    "true": "false",
    "false": "false",
  },
}

function f3<A extends Bool, B extends Bool>(a: A, b: B): And[A][B] {
    if (a === "true") {
      if (b === "true") {
        // no error
        return "true";
      } else {
        // no error
        return "false";
      }
    } else {
      if (b === "true") {
        // no error
        return "false";
      } else {
        // no error
        return "false";
      }
    }
}

function f4<A extends Bool, B extends Bool>(a: A, b: B): And[A][B] {
    if (a === "true") {
      if (b === "true") {
        // error
        return "false";
      } else {
        // error
        return "true";
      }
    } else {
      if (b === "true") {
        // error
        return "true";
      } else {
        // error
        return "true";
      }
    }
}

[damodharanj]

The above shows error for correct case

TS Version: 3.7.2

[rubenpieters]

Yes, the prototype implementation of dependent-type-like functions ( #33014 ) or things like it are not part of any TypeScript version at the moment. Hopefully in some future version functionality like this will be added to TypeScript.

[typescript-bot]

This issue has been marked 'Working as Intended' and has seen no recent activity. It has been automatically closed for house-keeping purposes.