3 ms·

I'm so lost. (I'm firmly in the static-typing camp, coming from an internal philosophy of "computers are supposed to do things as fast as possible, and not mak

by mrkeen 3y ago

I'm so lost. (I'm firmly in the static-typing camp, coming from an internal philosophy of "computers are supposed to do things as fast as possible, and not make mistakes".) > Intrinsic types are great because you are guaranteed to have a mathematically-sound safety net at all times. Sounds great, even if I take it with the usual grain of salt. > Extrinsic types are useful because you can apply multiple type systems to your code If I don't get the mathematically-sound safety net, why would I apply 1 type system to my code, let alone n?

layer8 3y ago
This lets different parts of your code use different type systems, so to speak, by picking and choosing which annotations you specify. Another real-life example is the “unsafe” mode some statically-typed languages have, which effectively switches to a laxer type system.
- zokier 3y ago
  > Another real-life example is the “unsafe” mode some statically-typed languages have, which effectively switches to a laxer type system. Are you referring to Rust here? Because I believe unsafe there doesn't change type checking or type system in any way
  - layer8 3y ago
    “Unsafe” disables borrow checking in Rust, which is part of the type system. C# also has a (different) “unsafe”.
    - neonsunset 3y ago
      Conceptually speaking they are quite close: both let you write code C-style with raw pointers within unsafe blocks. Similar to Rust, C# also has a subset of Unsafe and Marshal APIs which explicitly indicate their risk for bypassing compiler or language checks when either you know what you are doing or when whatever goal they achieve is not expressible with safe code.
    - remexre 3y ago
      unsafe does not disable the borrow checker, it allows calling functions that could not be otherwise written in code that is OK'd by the borrow checker.
zokier 3y ago
> If I don't get the mathematically-sound safety net, why would I apply 1 type system to my code, let alone n? I don't it is intended to imply that extrisic type systems wouldn't be sound. As for why you'd want several type systems, one benefit I imagine is that different type systems could verify different aspects of your program, instead of forcing to cram everything into one type system. Afaik just because type system is sound doesn't alone mean that it can be used practically to prove every interesting property of a program.
epgui 3y ago
This is actually a rare instance of the grain of salt being unnecessary. Depending on the type system, it is possible for it to guarantee that the only source of error be in your specification and not in your implementation.

by mrkeen 3y ago

layer8 3y ago

This lets different parts of your code use different type systems, so to speak, by picking and choosing which annotations you specify. Another real-life example is the “unsafe” mode some statically-typed languages have, which effectively switches to a laxer type system.

zokier 3y ago
> Another real-life example is the “unsafe” mode some statically-typed languages have, which effectively switches to a laxer type system. Are you referring to Rust here? Because I believe unsafe there doesn't change type checking or type system in any way
- layer8 3y ago
  “Unsafe” disables borrow checking in Rust, which is part of the type system. C# also has a (different) “unsafe”.
  - neonsunset 3y ago
    Conceptually speaking they are quite close: both let you write code C-style with raw pointers within unsafe blocks. Similar to Rust, C# also has a subset of Unsafe and Marshal APIs which explicitly indicate their risk for bypassing compiler or language checks when either you know what you are doing or when whatever goal they achieve is not expressible with safe code.
  - remexre 3y ago
    unsafe does not disable the borrow checker, it allows calling functions that could not be otherwise written in code that is OK'd by the borrow checker.

zokier 3y ago

> If I don't get the mathematically-sound safety net, why would I apply 1 type system to my code, let alone n? I don't it is intended to imply that extrisic type systems wouldn't be sound. As for why you'd want several type systems, one benefit I imagine is that different type systems could verify different aspects of your program, instead of forcing to cram everything into one type system. Afaik just because type system is sound doesn't alone mean that it can be used practically to prove every interesting property of a program.

epgui 3y ago

This is actually a rare instance of the grain of salt being unnecessary. Depending on the type system, it is possible for it to guarantee that the only source of error be in your specification and not in your implementation.