Kotlin's Type System is (Also) Unsound

• URL: http://arxiv.org/abs/2408.10804v1
• Date: Tue, 20 Aug 2024 12:54:12 GMT
• Title: Kotlin's Type System is (Also) Unsound
• Abstract summary: A type checker for a sound type system is expected to issue a warning on every type error. In 2016, Amin and Tate presented the first unsoundness proof for two major industry languages: Java and Scala. We present an unsoundness proof for Kotlin, which relies on a previously unknown unsound combination of language features.
• Score: 0.19116784879310028
• License: http://creativecommons.org/licenses/by-sa/4.0/
• Abstract: Soundness of a type system is a fundemental property that guarantees that no operation that is not supported by a value will be performed on that value at run time. A type checker for a sound type system is expected to issue a warning on every type error. While soundness is a desirable property for many practical applications, in 2016, Amin and Tate presented the first unsoundness proof for two major industry languages: Java and Scala. This proof relied on use-site variance and implicit null values. We present an unsoundness proof for Kotlin, another emerging industry language, which relies on a previously unknown unsound combination of language features. Kotlin does not have implicit null values, meaning that the proof by Amin and Tate would not work for Kotlin. Our new proof, which is an infringing code snippet, utilizes Kotlin's \emph{declaration-site} variance specification and does not require implicit null values. We present this counterexample to soundness in full along with detailed explanations of every step. Finally, we present a thorough discussion on precisely which language features cause this issue, as well as how Kotlin's compiler can be patched to fix it.

Related papers

• The Sound of Absence: Audio-Language Embedding Models Struggle with Negation [58.04745279785462]
  We show that embedding models fail to encode negated sound concepts.<n>We introduce NegEval-Audio, a framework that converts datasets into two negation-aware tasks.
  arXiv  Detail & Related papers  (2026-07-14T02:55:00Z)
• A Minimal Executable Proof for Multi-Language Contract Traceability [0.0]
  This paper reports a deliberately small executable proof for a DAG-TOML contract.<n>It shows how a contract, implementation graph, traceability chain, and review gate can be checked against executable witnesses.
  arXiv  Detail & Related papers  (2026-05-27T14:37:26Z)
• Type-Constrained Code Generation with Language Models [51.03439021895432]
  Large language models (LLMs) produce uncompilable output because their next-token inference procedure does not model formal aspects of code. We introduce a type-constrained decoding approach that leverages type systems to guide code generation. Our approach reduces compilation errors by more than half and increases functional correctness in code synthesis, translation, and repair tasks.
  arXiv  Detail & Related papers  (2025-04-12T15:03:00Z)
• LitmusKt: Concurrency Stress Testing for Kotlin [0.8312192184427764]
  We present LitmusKt - the first tool for testing concurrent programs in Kotlin. Our tool allows litmus tests in a single custom DSL, and these tests are then run in Kotlin/Native and Kotlin/JVM. Using LitmusKt, we discovered novel bugs in the Kotlin compiler, which we then fixed and they are no longer present.
  arXiv  Detail & Related papers  (2025-01-13T16:40:34Z)
• Generating Diverse Negations from Affirmative Sentences [0.999726509256195]
  Negations are important in real-world applications as they encode negative polarity in verb phrases, clauses, or other expressions. We propose NegVerse, a method that tackles the lack of negation datasets by producing a diverse range of negation types. We provide new rules for masking parts of sentences where negations are most likely to occur, based on syntactic structure. We also propose a filtering mechanism to identify negation cues and remove degenerate examples, producing a diverse range of meaningful perturbations.
  arXiv  Detail & Related papers  (2024-10-30T21:25:02Z)
• How Do Developers Use Type Inference: An Exploratory Study in Kotlin [3.382017614888546]
  Kotlin is the default language for Android development, one of the largest software marketplaces. We conduct a large-scale empirical study using Boa, a tool for mining software repositories. Our findings reveal that type inference is frequently employed for local variables and variables with method calls declared outside the file.
  arXiv  Detail & Related papers  (2024-10-30T18:07:21Z)
• Cross-Language Dependencies: An Empirical Study of Kotlin-Java [1.5680371708311132]
  Since Google introduced Kotlin as an official programming language for developing Android apps in 2017, Kotlin has gained widespread adoption in Android development. There is limited research on how Java and Kotlin interact with each other in real-world projects. We conducted an empirical study of 23 Kotlin-Java real-world projects with 3,227 Java and 8,630 Kotlin source files.
  arXiv  Detail & Related papers  (2024-05-07T18:26:24Z)
• Depends-Kotlin: A Cross-Language Kotlin Dependency Extractor [3.0915964434574175]
  Depends-Kotlin supports extracting entities' dependencies in Kotlin code. It can also extract dependency relations between Kotlin and Java. Depends-Kotlin demonstrates high accuracy and performance in resolving Kotlin-Kotlin and Kotlin-Java dependencies relations.
  arXiv  Detail & Related papers  (2024-01-30T10:15:35Z)
• PTE: Axiomatic Semantics based Compiler Testing [7.203331838793759]
  We propose an axiomatic semantics based approach for testing compilers, called PTE. The idea is to incrementally develop a set of axioms'' capturing anecdotes of the language semantics in the form of emph(textbfprecondition, textbftransformation, textbfexpectation''
  arXiv  Detail & Related papers  (2024-01-02T04:50:47Z)
• Generative Type Inference for Python [62.01560866916557]
  This paper introduces TypeGen, a few-shot generative type inference approach that incorporates static domain knowledge from static analysis. TypeGen creates chain-of-thought (COT) prompts by translating the type inference steps of static analysis into prompts based on the type dependency graphs (TDGs) Experiments show that TypeGen outperforms the best baseline Type4Py by 10.0% for argument type prediction and 22.5% in return value type prediction in terms of top-1 Exact Match.
  arXiv  Detail & Related papers  (2023-07-18T11:40:31Z)
• Efficient Semiring-Weighted Earley Parsing [71.77514972816347]
  This paper provides a reference description, in the form of a deduction system, of Earley's (1970) context-free parsing algorithm with various speed-ups. Our presentation includes a known worst-case runtime improvement from Earley's $O (N3|GR|)$, which is unworkable for the large grammars that arise in natural language processing. We treat the generalization to semiring-weighted deduction, preprocessing the grammar like Stolcke (1995) to eliminate deduction cycles, and further generalize Stolcke's method to compute the weights of sentence prefixes.
  arXiv  Detail & Related papers  (2023-07-06T13:33:59Z)
• Lexinvariant Language Models [84.2829117441298]
  Token embeddings, a mapping from discrete lexical symbols to continuous vectors, are at the heart of any language model (LM) We study textitlexinvariantlanguage models that are invariant to lexical symbols and therefore do not need fixed token embeddings in practice. We show that a lexinvariant LM can attain perplexity comparable to that of a standard language model, given a sufficiently long context.
  arXiv  Detail & Related papers  (2023-05-24T19:10:46Z)
• TypeT5: Seq2seq Type Inference using Static Analysis [51.153089609654174]
  We present a new type inference method that treats type prediction as a code infilling task. Our method uses static analysis to construct dynamic contexts for each code element whose type signature is to be predicted by the model. We also propose an iterative decoding scheme that incorporates previous type predictions in the model's input context.
  arXiv  Detail & Related papers  (2023-03-16T23:48:00Z)
• Multi-VALUE: A Framework for Cross-Dialectal English NLP [49.55176102659081]
  Multi- Dialect is a controllable rule-based translation system spanning 50 English dialects. Stress tests reveal significant performance disparities for leading models on non-standard dialects. We partner with native speakers of Chicano and Indian English to release new gold-standard variants of the popular CoQA task.
  arXiv  Detail & Related papers  (2022-12-15T18:17:01Z)
• Not another Negation Benchmark: The NaN-NLI Test Suite for Sub-clausal Negation [59.307534363825816]
  Negation is poorly captured by current language models, although the extent of this problem is not widely understood. We introduce a natural language inference (NLI) test suite to enable probing the capabilities of NLP methods.
  arXiv  Detail & Related papers  (2022-10-06T23:39:01Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.