3 ms·

I think the problem with what F* is doing is that it’s so foreign to most people that they don’t actually understand it. Typescript cannot do what you’re sayin

I think the problem with what F* is doing is that it’s so foreign to most people that they don’t actually understand it. Typescript cannot do what you’re saying at compile time. F* knows _at compile time_ whether or not a value is within a range, and you can get a compiler error _without executing the program_.

eyelidlessness 6y ago
TypeScript can do that. That’s what I was saying.
- indolering 6y ago
  I'm pretty sure TypeScript 4 didn't add support for dependent types. Please cite your source or include a link to source code : ).
- amw-zero 6y ago
  Please provide a code example.
  - eyelidlessness 6y ago
    This was my proof of concept for non-negative integers. You can clearly use the "template literal type" functionality to do arbitrary type processing. People have used it for JSON, SQL and GraphQL type validation. Validating a numerical range is trivial compared to those. type IntegerChar = | '0' | '1' | '2' | '3' | '4' | '5' | '6' | '7' | '8' | '9'; type IntegerString<T extends string> = T extends IntegerChar ? T : T extends `${infer Char}${infer Rest}` ? Char extends IntegerChar ? Rest extends IntegerString<Rest> ? `${Char}${Rest}` : never : never : never; type NonNegativeInteger<T extends number> = T extends infer U ? number extends U ? never : `${U}` extends IntegerChar ? U : `${U}` extends IntegerString<`${U}`> ? U : never : never; type NonNegativeInteger<T extends number> = T extends infer U ? number extends U ? never : `${U}` extends IntegerChar ? U : `${U}` extends IntegerString<`${U}`> ? U : never : never;
    - amw-zero 6y ago
      It’s not difficult when you can enumerate every member of a type. Can you write a type for prime numbers this way?
      - eyelidlessness 6y ago
        I didn’t enumerate every member though, just the digit. I’m sure it’s possible to calculate primes. The TS type system has been turing complete since 2.something, it’s just easier to use now. Edit to add: they don’t use semver, they just roll over at 9, so it’s been turning complete for ~20 releases.
        amw-zero 6y ago
        In poking around, I found this: https://github.com/microsoft/TypeScript/issues/14833 https://github.com/microsoft/TypeScript/issues/14833 Where someone actually implements a compile-time check for prime numbers. I guess saying that it _can't_ be done is inaccurate. It's just absolutely horrendous.
        eyelidlessness 6y ago
        Right that issue was in mind in my last comment. But that was almost 4 years ago, and the type system has become a lot more capable. Including the template literal types as used in my dumb little non-negative int or in compile time JSON, SQL and GraphQL parsing. Which are still horrendous but a great deal less so than some of the hacks from 2027, and a lot easier to read. It’s definitely not an ML type system, but I’d bet a dollar it takes more inspiration and guidance from F# than C#.

eyelidlessness 6y ago

TypeScript can do that. That’s what I was saying.

indolering 6y ago
I'm pretty sure TypeScript 4 didn't add support for dependent types. Please cite your source or include a link to source code : ).
amw-zero 6y ago
Please provide a code example.
- eyelidlessness 6y ago
  This was my proof of concept for non-negative integers. You can clearly use the "template literal type" functionality to do arbitrary type processing. People have used it for JSON, SQL and GraphQL type validation. Validating a numerical range is trivial compared to those. type IntegerChar = | '0' | '1' | '2' | '3' | '4' | '5' | '6' | '7' | '8' | '9'; type IntegerString<T extends string> = T extends IntegerChar ? T : T extends `${infer Char}${infer Rest}` ? Char extends IntegerChar ? Rest extends IntegerString<Rest> ? `${Char}${Rest}` : never : never : never; type NonNegativeInteger<T extends number> = T extends infer U ? number extends U ? never : `${U}` extends IntegerChar ? U : `${U}` extends IntegerString<`${U}`> ? U : never : never; type NonNegativeInteger<T extends number> = T extends infer U ? number extends U ? never : `${U}` extends IntegerChar ? U : `${U}` extends IntegerString<`${U}`> ? U : never : never;
  - amw-zero 6y ago
    It’s not difficult when you can enumerate every member of a type. Can you write a type for prime numbers this way?
    - eyelidlessness 6y ago
      I didn’t enumerate every member though, just the digit. I’m sure it’s possible to calculate primes. The TS type system has been turing complete since 2.something, it’s just easier to use now. Edit to add: they don’t use semver, they just roll over at 9, so it’s been turning complete for ~20 releases.
      - amw-zero 6y ago
        In poking around, I found this: https://github.com/microsoft/TypeScript/issues/14833 https://github.com/microsoft/TypeScript/issues/14833 Where someone actually implements a compile-time check for prime numbers. I guess saying that it _can't_ be done is inaccurate. It's just absolutely horrendous.
        eyelidlessness 6y ago
        Right that issue was in mind in my last comment. But that was almost 4 years ago, and the type system has become a lot more capable. Including the template literal types as used in my dumb little non-negative int or in compile time JSON, SQL and GraphQL parsing. Which are still horrendous but a great deal less so than some of the hacks from 2027, and a lot easier to read. It’s definitely not an ML type system, but I’d bet a dollar it takes more inspiration and guidance from F# than C#.