6 ms·

Static Type Checking in Common Lisp

161 points by mr_tyzic 7y ago

hyperion2010 7y ago
Fantastic. Apparently I am not the only one that has been digging around for more detailed information about how CL implements static typing. There is so much FUD out there from the ??? community(ies) that I ended up sitting down and finding the relevant sections in my lab's copy of CLTL2. This article does an excellent job of laying out the consequences of the standard in a way that is clear and understandable, and probably that also includes knowledge about those consequences that was not entirely known at the time (or maybe it was, but just not documented). I kind of wish the author had named his type defun `defunct` though!
- dreamcompiler 7y ago
  As reikonomusha points out, this article is highly SBCL-specific. Other Common Lisps typically use type declarations more as reasons not to check types at runtime. SBCL on the other hand also uses type declarations to reason about types at compile time.
lisper 7y ago
I hereby inaugurate Ron's third law: for any perceived shortcoming of Common Lisp you can write a macro that fixes it for less effort than it takes to complain about it.
- reikonomusha 7y ago
  It’s a romantic idea but it’s simply not true. I have two examples. The first example is easy: Implement an O(1) jump table in Common Lisp that respects the lexical environment. (You can’t, unless CASE is itself optimized to a jump table, which it usually isn’t.) The second example: Consider the SAME-FRINGE [0] problem. You’ll have a hard time macro-ing your way out of that unless your Lisp implementation has a built-in API for coroutines [1], or you write extraordinarily difficult macros to CPS-convert the entirety of Common Lisp to allow for CALL/CC. The latter is itself a hefty project to do well. This is not to say SAME-FRINGE can’t be solved in Lisp. It can. The page I linked has several solutions in Common Lisp. But idiomatic solutions are consy and inefficient. For instance, the usual SICP hack to write lazy sequences with thunks “works”, but doesn’t deeply integrate with the rest of Lisp so easily. And coroutine/CPS libraries in Lisp often have a bag of gotchas (e.g., they don’t work with high-order functions like MAPCAR). While I understand this is subjective, the most natural solution to this problem uses a control mechanism that just doesn’t exist in Common Lisp. [0] http://wiki.c2.com/?SameFringeProblem http://wiki.c2.com/?SameFringeProblem [1] Many Lisps used to, but it has fallen by the wayside since Lisps began to support native OS threads.
  - gumby 7y ago
    > The first example is easy: Implement an O(1) jump table in Common Lisp that respects the lexical environment. (You can’t, unless CASE is itself optimized to a jump table, which it usually isn’t.) Perhaps I don't understand your objection: you can certainly store any object in an array and funcall it which would be O(1); the object could be a lambda that captured the lexical environment. I was doing that 35 years ago on the lisp machine Interestingly I did this also on the D-Machine Interlisp and each closure forked the stack, so it ground the machine to a halt, a design bug later fixed. Both examples I'm talking about predate Common Lisp standardization.
    - ohyes 7y ago
      For the true jump table experience Tagbody / go would also work just fine for this. You can put the ‘go’s in lambdas in an array and funcall them. This sounds like fun.
      - reikonomusha 7y ago
        Not so. The table of lambdas have to be built at runtime, making it O(N). You can’t use LOAD-TIME-VALUE because that doesn’t respect the lexical environment, which TAGBODY tags live in.
        ohyes 7y ago
        Well, you have to make the go statement in lexical scope in order for the tagbody to work... that seems reasonable enough to me. You specifically stated: > Implement an O(1) jump table in Common Lisp that respects the lexical environment. You don't know the lexical environment until there's a lexical environment to know, you can't have your cake and also eat it (or not have your cake and also know it). Interestingly, try/catch also solves this problem fairly elegantly without distastefully consing up a list or array at run-time. (defun jump2 (i) (let ((location nil)) (tagbody (catch 'a (catch 'b (catch 'c (catch 'd (setf location (elt #(a b c d) i)) (throw location nil)) (when location (print "D!") (go end))) (when location (print "C!") (go end))) (when location (print "B!") (go end))) (when location (print "A!") (go end)) end))) I'll leave the relevant macro to the reader, it shouldn't be that difficult... (I'm hoping I didn't just do someone's homework). edit: removed some cruft from experiments and fixed formatting
choeger 7y ago
Of course you can invoke a type checker inside a language with compile time macros. Did anyone ever doubt that? The interesting question is: what does that type checker actually check? How does it deal with normal lisp functions? How is non-trivial data represented? And what happens when it stumbles upon a runtime macro? And, on a more practical side, how does it access the environment?
- jjnoakes 7y ago
  This article is more about taking an existing type-checking system (http://www.sbcl.org/manual/#Handling-of-Types http://www.sbcl.org/manual/#Handling-of-Types) and adding some syntactic sugar so you can declare the types inline, similar to other languages, instead of separately.
- deleted 7y ago
  [deleted]
- Jach 7y ago
  The type checker checks types. SBCL's type inference is based on Kaplan-Ullman, rather than Hindley-Milner (see https://news.ycombinator.com/item?id=12216701 https://news.ycombinator.com/item?id=12216701). A remark from the linked paper there to keep in mind: "There has been some confusion about the difference between type checking for the purposes of compiling traditional languages, and type checking for the purposes of ensuring a program's correctness." The big caveat with this post is that while types and type declarations are part of the standard, doing what SBCL does to infer them beyond what's declared or handle them for purposes of compile-time warnings and optimized assembly code generation is up to a Common Lisp implementation and others that aren't SBCL (or older SBCL versions, or programs that declare things like (safety 0) to turn off type checks) may behave differently. Normal lisp functions can have more restrictive types than T, too. Typing (describe 'symbol) for a function will have SBCL say (among other things) that the symbol names a compiled function with a certain argument list, declared type, and derived type. (There's a distinction because I might have declared the function parameter a to be type (integer 0 255) which SBCL simplifies to (unsigned-byte 8).) SBCL has a convenient way to get the derived type info as a list that might be useful for macros or editor extensions, it works for your functions or standard functions e.g. the standard string-to-uppercase function as provided by SBCL has the type: (sb-introspect:function-type #'string-upcase) (FUNCTION ((OR (VECTOR CHARACTER) (VECTOR NIL) BASE-STRING SYMBOL CHARACTER) &KEY (:START (MOD 4611686018427387901)) (:END (OR NULL (MOD 4611686018427387901)))) (VALUES SIMPLE-STRING &OPTIONAL)) i.e. it takes a string (among other possibilities), some optional non-negative integer keyword parameters (up to some max number, which is 2 smaller than my system's most-positive-fixnum value), and outputs a simple-string. This might lead to developing an interesting IDE tool / slime extension that lets you "tab complete" a variable by asking the system what functions you can call that expect the type of the variable's value as the first argument. (slime basically already has this with "who specializes" for finding generic functions.) You can define your own types with (deftype) for non-trivial data. (Or even trivial data like an enum type: (deftype valid-color () `(member :red :green :blue)) Depending on how non-trivial it is, this may impair optimization opportunities or the compiler being able to notice type mismatches (though you can tell the compiler to give you a notice about type uncertainties), so you're back to runtime checking. Runtime macros talk to the compiler to generate code, same as compile-time macros. The compiler never goes away in runtime (without some effort in extracting it from the final deliverable anyway) -- COMPILE is a standard compiled function -- which makes it possible to e.g. interactively debug an erroring function, recompile a fixed version that everything will now call instead, all from 100 million miles away back on earth. What do you mean by "the environment"?
johnisgood 7y ago
I have to say these type of articles make me want to get into Common Lisp again. Good stuff, thanks! :)
- johnisgood 7y ago
  I ended up looking around Racket because it seems to have better libraries. My problems so far are: - lack of (loop), (dotimes), etc. - lack of (restart-case), (invoke-restart), etc. - REPL feels extremely different from SBCL's one (or emacs + SLIME + SBCL), it is definitely non-Lispy - inconsistent naming (e.g. see (path-get-extension) and (file-name-from-path) where in other libraries it is "filename" not "file-name" hence the inconsistency, and the "get" in (path-get-extension) seems odd. There is a deprecated (filename-extension), I think sticking to that would be better. I know that backwards-compatibility is the issue but cannot we just issue a warning for a few releases instead?) - (time) is much less informative than SBCL's (time) - this is really subjective, but I prefer (progn) over (begin) In my opinion Racket is better in some regards than Common Lisp, but it still has its warts. Common Lisp has its own warts. I really wish that these issues were to be resolved somehow in Racket so I could have my "perfect" language. :(
  - johnisgood 7y ago
    Apparently there is no (disassemble) either. :/ I am using https://github.com/samth/disassemble https://github.com/samth/disassemble for now.
  - soegaard 7y ago
    FWIW the `control` packages contains versions of `dotimes` and `tagbody`. https://docs.racket-lang.org/control-manual/index.html https://docs.racket-lang.org/control-manual/index.html Make an issue with regards to the filename inconsistency. I hadn't noticed before - and had to look it up. The confusion stems in the fact that both "file name" and "filename" count as correct spelling (sigh). Wrt to `time` take a look at the `benchmark` package: https://docs.racket-lang.org/benchmark/index.html https://docs.racket-lang.org/benchmark/index.html
    - 7y ago
deleted 7y ago
[deleted]
reikonomusha 7y ago
Hopefully nobody reading the article ends up disappointed knowing that the type checking presented is SBCL-only, working only for a subset of the Common Lisp type system (which itself is large and elaborate), with only informal guarantees of compile-time support, and doesn’t come close to allowing any sort of type checking with polymorphism or sum-types involved. None of those take away from the value SBCL’s type checking provides; the features presented do catch real bugs in real code, and I’d prefer those features are there than not there. If you are disappointed, however, then... Coalton [1] is a project that adds tried-and-true Hindley-Milner type checking to Common Lisp which allows for gradual adoption, in the same way Typed Racket or Hack allows for. You can think of Coalton as an embedded DSL in Lisp that resembles Standard ML or OCaml, but lets you seamlessly interoperate with non-statically-typed Lisp code (and vice versa). It’s really intended as a practical tool to allow parts or most of your codebase to be statically typed, without compromising the dynamic and interactive nature of Common Lisp. On top of it all you get all of the facilities of Lisp, like macros, compile-time evaluation, etc. Coalton code is truly Lisp code, it’s just—at the end of the day—extra syntax to allow a type checker (also Lisp!) to run. As a benefit, it allows quasi-trivial porting of ML-like code to Lisp. Almost all ML construct has a direct correspondence in Coalton. It’s still a work in progress, especially in terms of polish and documentation, but it works. Shen [2] is another interesting project, but I didn’t generally find it very compatible with the ML style of program construction, and it seemed to have goals diverging from being an extension of Lisp, into being some hyper-portable independent language. [1] https://github.com/stylewarning/coalton https://github.com/stylewarning/coalton [2] http://www.shenlanguage.org/ http://www.shenlanguage.org/
- gumby 7y ago
  MACLISP had state of the art type checking and compiler optimization, for the 1970s state of the art, and produced better math code than I could write by hand in assembler. These capabilities were used extensively for MACSYMA. The point of the article wasn't to say that all common lisps support type declaration but to show how easy it is to add support for such decoration (and optional support to boot). Arbitrary amounts of inference could be added in such declarations before feeding the result to the compiler; the same work could be easily extended for other compilers -- and that other pre-analysis would work there too.
bjourne 7y ago
This method of adding static typing to a dynamically typed language is called gradual typing. It works and is sound but can come at a considerable cost if the compiler doesn't support it well. Suppose that you have function that you know only returns fixnum, but isn't declared as such, and you use that result as the input to a function declared to only take fixnum then the compiler has to add runtime type checks. Even very cheap type checks can cause massive overhead if they are executed in tight loops. Or suppose the fixnum x is given as input to an identity function: (id x). The compiler knows that x is a fixnum, but unless it is sufficiently smart it has no idea that (id x) is one too.
- juki 7y ago
  This problem is somewhat lessened because SBCL also allows you to tell it to not add any implicit runtime type checks (explicit checks are still there) with an `(optimize (safety 0))` declaration. Of course, then you have to be sure that the code is indeed safe, so you probably don't want it as a global declaration, but only locally for the tight loops. When optimizing for speed SBCL also gives warnings for generic arithmetic, so you can add the necessary declarations.
  - bjourne 7y ago
    Sure, but then you lose soundness. That is, it becomes possible to fool the compiler into thinking, say, a string is a fixnum, leading to crashes. It becomes equivalent to the optional typing of mypy which also is easy too fool because it doesn't insert any type checks. def oh(): return 'hi' x: int = oh() x + 3 It type checks fine but contains a type error.
    - juki 7y ago
      You don't lose soundness; you just tell the compiler to not check types at run time, because you've already done it yourself (e.g. by not exposing the unsafe code directly outside the package, but instead having a safe wrapper around it). This isn't really any different from using unsafe/foreign code in a statically typed language.

161 points by mr_tyzic 7y ago

hyperion2010 7y ago

Fantastic. Apparently I am not the only one that has been digging around for more detailed information about how CL implements static typing. There is so much FUD out there from the ??? community(ies) that I ended up sitting down and finding the relevant sections in my lab's copy of CLTL2. This article does an excellent job of laying out the consequences of the standard in a way that is clear and understandable, and probably that also includes knowledge about those consequences that was not entirely known at the time (or maybe it was, but just not documented). I kind of wish the author had named his type defun `defunct` though!

dreamcompiler 7y ago
As reikonomusha points out, this article is highly SBCL-specific. Other Common Lisps typically use type declarations more as reasons not to check types at runtime. SBCL on the other hand also uses type declarations to reason about types at compile time.

lisper 7y ago

I hereby inaugurate Ron's third law: for any perceived shortcoming of Common Lisp you can write a macro that fixes it for less effort than it takes to complain about it.

reikonomusha 7y ago
It’s a romantic idea but it’s simply not true. I have two examples. The first example is easy: Implement an O(1) jump table in Common Lisp that respects the lexical environment. (You can’t, unless CASE is itself optimized to a jump table, which it usually isn’t.) The second example: Consider the SAME-FRINGE [0] problem. You’ll have a hard time macro-ing your way out of that unless your Lisp implementation has a built-in API for coroutines [1], or you write extraordinarily difficult macros to CPS-convert the entirety of Common Lisp to allow for CALL/CC. The latter is itself a hefty project to do well. This is not to say SAME-FRINGE can’t be solved in Lisp. It can. The page I linked has several solutions in Common Lisp. But idiomatic solutions are consy and inefficient. For instance, the usual SICP hack to write lazy sequences with thunks “works”, but doesn’t deeply integrate with the rest of Lisp so easily. And coroutine/CPS libraries in Lisp often have a bag of gotchas (e.g., they don’t work with high-order functions like MAPCAR). While I understand this is subjective, the most natural solution to this problem uses a control mechanism that just doesn’t exist in Common Lisp. [0] http://wiki.c2.com/?SameFringeProblem http://wiki.c2.com/?SameFringeProblem [1] Many Lisps used to, but it has fallen by the wayside since Lisps began to support native OS threads.
- gumby 7y ago
  > The first example is easy: Implement an O(1) jump table in Common Lisp that respects the lexical environment. (You can’t, unless CASE is itself optimized to a jump table, which it usually isn’t.) Perhaps I don't understand your objection: you can certainly store any object in an array and funcall it which would be O(1); the object could be a lambda that captured the lexical environment. I was doing that 35 years ago on the lisp machine Interestingly I did this also on the D-Machine Interlisp and each closure forked the stack, so it ground the machine to a halt, a design bug later fixed. Both examples I'm talking about predate Common Lisp standardization.
  - ohyes 7y ago
    For the true jump table experience Tagbody / go would also work just fine for this. You can put the ‘go’s in lambdas in an array and funcall them. This sounds like fun.
    - reikonomusha 7y ago
      Not so. The table of lambdas have to be built at runtime, making it O(N). You can’t use LOAD-TIME-VALUE because that doesn’t respect the lexical environment, which TAGBODY tags live in.
      - ohyes 7y ago
        Well, you have to make the go statement in lexical scope in order for the tagbody to work... that seems reasonable enough to me. You specifically stated: > Implement an O(1) jump table in Common Lisp that respects the lexical environment. You don't know the lexical environment until there's a lexical environment to know, you can't have your cake and also eat it (or not have your cake and also know it). Interestingly, try/catch also solves this problem fairly elegantly without distastefully consing up a list or array at run-time. (defun jump2 (i) (let ((location nil)) (tagbody (catch 'a (catch 'b (catch 'c (catch 'd (setf location (elt #(a b c d) i)) (throw location nil)) (when location (print "D!") (go end))) (when location (print "C!") (go end))) (when location (print "B!") (go end))) (when location (print "A!") (go end)) end))) I'll leave the relevant macro to the reader, it shouldn't be that difficult... (I'm hoping I didn't just do someone's homework). edit: removed some cruft from experiments and fixed formatting

choeger 7y ago

Of course you can invoke a type checker inside a language with compile time macros. Did anyone ever doubt that? The interesting question is: what does that type checker actually check? How does it deal with normal lisp functions? How is non-trivial data represented? And what happens when it stumbles upon a runtime macro? And, on a more practical side, how does it access the environment?

jjnoakes 7y ago
This article is more about taking an existing type-checking system (http://www.sbcl.org/manual/#Handling-of-Types http://www.sbcl.org/manual/#Handling-of-Types) and adding some syntactic sugar so you can declare the types inline, similar to other languages, instead of separately.
deleted 7y ago
[deleted]
Jach 7y ago
The type checker checks types. SBCL's type inference is based on Kaplan-Ullman, rather than Hindley-Milner (see https://news.ycombinator.com/item?id=12216701 https://news.ycombinator.com/item?id=12216701). A remark from the linked paper there to keep in mind: "There has been some confusion about the difference between type checking for the purposes of compiling traditional languages, and type checking for the purposes of ensuring a program's correctness." The big caveat with this post is that while types and type declarations are part of the standard, doing what SBCL does to infer them beyond what's declared or handle them for purposes of compile-time warnings and optimized assembly code generation is up to a Common Lisp implementation and others that aren't SBCL (or older SBCL versions, or programs that declare things like (safety 0) to turn off type checks) may behave differently. Normal lisp functions can have more restrictive types than T, too. Typing (describe 'symbol) for a function will have SBCL say (among other things) that the symbol names a compiled function with a certain argument list, declared type, and derived type. (There's a distinction because I might have declared the function parameter a to be type (integer 0 255) which SBCL simplifies to (unsigned-byte 8).) SBCL has a convenient way to get the derived type info as a list that might be useful for macros or editor extensions, it works for your functions or standard functions e.g. the standard string-to-uppercase function as provided by SBCL has the type: (sb-introspect:function-type #'string-upcase) (FUNCTION ((OR (VECTOR CHARACTER) (VECTOR NIL) BASE-STRING SYMBOL CHARACTER) &KEY (:START (MOD 4611686018427387901)) (:END (OR NULL (MOD 4611686018427387901)))) (VALUES SIMPLE-STRING &OPTIONAL)) i.e. it takes a string (among other possibilities), some optional non-negative integer keyword parameters (up to some max number, which is 2 smaller than my system's most-positive-fixnum value), and outputs a simple-string. This might lead to developing an interesting IDE tool / slime extension that lets you "tab complete" a variable by asking the system what functions you can call that expect the type of the variable's value as the first argument. (slime basically already has this with "who specializes" for finding generic functions.) You can define your own types with (deftype) for non-trivial data. (Or even trivial data like an enum type: (deftype valid-color () `(member :red :green :blue)) Depending on how non-trivial it is, this may impair optimization opportunities or the compiler being able to notice type mismatches (though you can tell the compiler to give you a notice about type uncertainties), so you're back to runtime checking. Runtime macros talk to the compiler to generate code, same as compile-time macros. The compiler never goes away in runtime (without some effort in extracting it from the final deliverable anyway) -- COMPILE is a standard compiled function -- which makes it possible to e.g. interactively debug an erroring function, recompile a fixed version that everything will now call instead, all from 100 million miles away back on earth. What do you mean by "the environment"?

johnisgood 7y ago

I have to say these type of articles make me want to get into Common Lisp again. Good stuff, thanks! :)

johnisgood 7y ago
I ended up looking around Racket because it seems to have better libraries. My problems so far are: - lack of (loop), (dotimes), etc. - lack of (restart-case), (invoke-restart), etc. - REPL feels extremely different from SBCL's one (or emacs + SLIME + SBCL), it is definitely non-Lispy - inconsistent naming (e.g. see (path-get-extension) and (file-name-from-path) where in other libraries it is "filename" not "file-name" hence the inconsistency, and the "get" in (path-get-extension) seems odd. There is a deprecated (filename-extension), I think sticking to that would be better. I know that backwards-compatibility is the issue but cannot we just issue a warning for a few releases instead?) - (time) is much less informative than SBCL's (time) - this is really subjective, but I prefer (progn) over (begin) In my opinion Racket is better in some regards than Common Lisp, but it still has its warts. Common Lisp has its own warts. I really wish that these issues were to be resolved somehow in Racket so I could have my "perfect" language. :(
- johnisgood 7y ago
  Apparently there is no (disassemble) either. :/ I am using https://github.com/samth/disassemble https://github.com/samth/disassemble for now.
- soegaard 7y ago
  FWIW the `control` packages contains versions of `dotimes` and `tagbody`. https://docs.racket-lang.org/control-manual/index.html https://docs.racket-lang.org/control-manual/index.html Make an issue with regards to the filename inconsistency. I hadn't noticed before - and had to look it up. The confusion stems in the fact that both "file name" and "filename" count as correct spelling (sigh). Wrt to `time` take a look at the `benchmark` package: https://docs.racket-lang.org/benchmark/index.html https://docs.racket-lang.org/benchmark/index.html
  - 7y ago

deleted 7y ago

[deleted]

reikonomusha 7y ago

Hopefully nobody reading the article ends up disappointed knowing that the type checking presented is SBCL-only, working only for a subset of the Common Lisp type system (which itself is large and elaborate), with only informal guarantees of compile-time support, and doesn’t come close to allowing any sort of type checking with polymorphism or sum-types involved. None of those take away from the value SBCL’s type checking provides; the features presented do catch real bugs in real code, and I’d prefer those features are there than not there. If you are disappointed, however, then... Coalton [1] is a project that adds tried-and-true Hindley-Milner type checking to Common Lisp which allows for gradual adoption, in the same way Typed Racket or Hack allows for. You can think of Coalton as an embedded DSL in Lisp that resembles Standard ML or OCaml, but lets you seamlessly interoperate with non-statically-typed Lisp code (and vice versa). It’s really intended as a practical tool to allow parts or most of your codebase to be statically typed, without compromising the dynamic and interactive nature of Common Lisp. On top of it all you get all of the facilities of Lisp, like macros, compile-time evaluation, etc. Coalton code is truly Lisp code, it’s just—at the end of the day—extra syntax to allow a type checker (also Lisp!) to run. As a benefit, it allows quasi-trivial porting of ML-like code to Lisp. Almost all ML construct has a direct correspondence in Coalton. It’s still a work in progress, especially in terms of polish and documentation, but it works. Shen [2] is another interesting project, but I didn’t generally find it very compatible with the ML style of program construction, and it seemed to have goals diverging from being an extension of Lisp, into being some hyper-portable independent language. [1] https://github.com/stylewarning/coalton https://github.com/stylewarning/coalton [2] http://www.shenlanguage.org/ http://www.shenlanguage.org/

gumby 7y ago
MACLISP had state of the art type checking and compiler optimization, for the 1970s state of the art, and produced better math code than I could write by hand in assembler. These capabilities were used extensively for MACSYMA. The point of the article wasn't to say that all common lisps support type declaration but to show how easy it is to add support for such decoration (and optional support to boot). Arbitrary amounts of inference could be added in such declarations before feeding the result to the compiler; the same work could be easily extended for other compilers -- and that other pre-analysis would work there too.

bjourne 7y ago

This method of adding static typing to a dynamically typed language is called gradual typing. It works and is sound but can come at a considerable cost if the compiler doesn't support it well. Suppose that you have function that you know only returns fixnum, but isn't declared as such, and you use that result as the input to a function declared to only take fixnum then the compiler has to add runtime type checks. Even very cheap type checks can cause massive overhead if they are executed in tight loops. Or suppose the fixnum x is given as input to an identity function: (id x). The compiler knows that x is a fixnum, but unless it is sufficiently smart it has no idea that (id x) is one too.

juki 7y ago
This problem is somewhat lessened because SBCL also allows you to tell it to not add any implicit runtime type checks (explicit checks are still there) with an `(optimize (safety 0))` declaration. Of course, then you have to be sure that the code is indeed safe, so you probably don't want it as a global declaration, but only locally for the tight loops. When optimizing for speed SBCL also gives warnings for generic arithmetic, so you can add the necessary declarations.
- bjourne 7y ago
  Sure, but then you lose soundness. That is, it becomes possible to fool the compiler into thinking, say, a string is a fixnum, leading to crashes. It becomes equivalent to the optional typing of mypy which also is easy too fool because it doesn't insert any type checks. def oh(): return 'hi' x: int = oh() x + 3 It type checks fine but contains a type error.
  - juki 7y ago
    You don't lose soundness; you just tell the compiler to not check types at run time, because you've already done it yourself (e.g. by not exposing the unsafe code directly outside the package, but instead having a safe wrapper around it). This isn't really any different from using unsafe/foreign code in a statically typed language.