Questions tagged [type-systems]

Type systems impose constraints on what programs may be written, by providing a syntactic method for operating with those constraints.

Filter by
Sorted by
Tagged with
0 votes
1 answer
39 views

What does "w.r.t. " mean in Kotlin?

This word shows up many times in this web page : https://kotlinlang.org/spec/type-system.html#function-types Can anyone help me to find out where defines this word?
  • 5,329
0 votes
1 answer
89 views

Can assert a variable to be an instance of a String in Deno

Can't seem to be able to assert instances of string in Deno: import { assertInstanceOf } from "https://deno.land/std@0.174.0/testing/asserts.ts"; assertInstanceOf( "foo", string ...
  • 22k
0 votes
0 answers
54 views

In intuitionistic type theory, does system LambdaP2 always imply CoC?

Considering the lambda cube: https://en.wikipedia.org/wiki/Lambda_cube system Lambda-P2 is characterised by capabilities to support: (assuming that a,b,c are terms, X,Y,Z are types) term to type ...
  • 4,747
0 votes
0 answers
67 views

In scala3/dotty. Why is it impossible to mix in a type definition with constraint?

In some cases it make sense to reuse a type constraint in both refinement and definition. E.g. the following definitions for Thing1 & Thing2 should be extensionally equivalent: object TypeMixin { ...
  • 4,747
0 votes
0 answers
48 views

How to implement associated types in Python/Mypy? Or, what to do when wanting sub-classes to have subclass arguments?

Consider the (simplified) code, where I want Lean* and Isabelle* extend the Base*. class BaseProblem: ... class BaseStep: ... class LeanProblem(BaseProblem): ... class LeanStep(BaseStep): ... class ...
  • 15.1k
1 vote
1 answer
47 views

TS check if Type contains 'null' Type

I have the following both Typescript Types defined. One of the type contains nullthe other neither. Is it possible to check such type for the existence of null? type TransactionCategory = "B2B&...
  • 73
0 votes
1 answer
185 views

What is the Haskell equivalence of Rust's associated types?

What is the Haskell equivalence of Rust's associated types?
  • 159
9 votes
5 answers
336 views

Why is char different from *both* signed char and unsigned char?

cppreference.com states that char is Equivalent to either signed char or unsigned char [...], but char is a distinct type, different from both signed char and unsigned char I assume this means that ...
  • 394
0 votes
1 answer
162 views

How to model several types with parent-child relationships and chaining methods which all extend the same base class?

I am trying to create and model the types for a series of classes which can be called in a chain in order to execute a method on the deepest class. Each of these classes represents a resource, and ...
  • 155
0 votes
1 answer
102 views

function types with generics and function expressions

Say I have the definition of a generic function that does something to a value of type T: function doSomething<T> (t: T): void { // do something on a value of type T console.log(t); } ...
0 votes
1 answer
35 views

Is Python's flexibility in the types of list elements a consequence of dynamic typing?

I am new to Python with some experience in C++. (Unfortunately, with just two sample points, any pair of features are either uncorrelated or perfectly correlated.) In Python, the elements in the same ...
  • 337
2 votes
1 answer
144 views

Modelling the composition of units (e.g. Inch, Dollar, etc) in Haskell

Following up from a previous question of mine, where I asked how I could create a type that would model a unit (e.g. Inch) as a type in Haskell, I now face the problem of how to perform operations on ...
  • 2,903
2 votes
1 answer
160 views

F# error: "Either make the arguments to 'it' explicit or, if you do not intend for it to be generic, add a type annotation."

In F# interactive shell dotnet fsi, I'm trying to test flip function as in Haskell, flip :: (a -> b -> c) -> b -> a -> c > let flip = fun f -> fun a -> fun b -> f(b)(a);; ...
-1 votes
1 answer
77 views

Why java type erasure is needed at runtime at all?

Below is an excerpt from java documentation here Because of type erasure, List<Number> and List<String> both become List. Consequently, the compiler allows the assignment of the object l, ...
  • 531
2 votes
2 answers
505 views

Why is KFunction2 not a denotable type in Kotlin?

Let's assume we have the following class in Kotlin (version 1.6.21, targeting JVM 17): interface Cursor( fun seekOrNext(target: String): Boolean fun seekOrPrevious(target: String): Boolean ) ...
0 votes
2 answers
74 views

match against template template type parameter

Say I would like to type-match any container with a specific member (a constraint) - but also bind type variables to both the container and the member. For example let T and U be the template type ...
  • 1,843
0 votes
1 answer
105 views

deferred selection of types during compile-time

Is there a standard way for me to select a type at compile-time in c++20 when the type depends on compile-time information available later in the function, i.e. the type is "deferred" ...
  • 1,843
3 votes
0 answers
35 views

Why does the lenght of tuple types change on intersection?

I have a little project to build a wrapper class for JavaScript numbers, such supports more specific types (PositveInteger, NotNegativeNumber, NotZeroNumber ...). While coding I found this curio: If I ...
  • 61
1 vote
0 answers
12 views

Does mutation break contravariance in the same way it breaks covariance?

Mutative covariant containers are unsound. For example, and using no language in particular, interface Pet; class Cat extends Pet { meow(); } class Dog extends Pet { woof(); } class Box[T] { value: ...
  • 1,969
4 votes
2 answers
96 views

Can't create recursive type `using T = vector<T::iterator>`

I'm trying to create a vector that contains its own iterators as elements, and I find it impossible to fully expand the type declaration. using MyVectorType = std::vector<std::vector<...>::...
  • 4,031
0 votes
1 answer
76 views

[F#][Type inference] - How to improve my program?

I'm currently building a program to type inference in F# using the following AST: // errors // exception SyntaxError of string * FSharp.Text.Lexing.LexBuffer<char> exception TypeError of string ...
  • 38
2 votes
1 answer
218 views

Extract specific parts from sentence by using infer keyword in Typescript Template Literal?

Assume inputting a sentence contains one or two spaces and has the structure ${Verb}${one or two spaces}${Activity}, how could I extract the Verb and Activity in Typescript? type Split = ' ' | ' ' ...
  • 633
4 votes
0 answers
116 views

HMF inference for recursive functions

I'm working on an implementation of the HMF type system described in this paper by Daan Leijen. The inference algorithm for HMF is defined in section 6.3. Here is the rule for let expressions (...
4 votes
3 answers
136 views

Rigid type variable -- why no error appears?

In the following example I'm internally implementing the function f. Its signature is using a as if the type variable a is scoped, and it is working without giving me a compile error even though I ...
13 votes
3 answers
700 views

Are codatatypes really terminal algebras?

(Disclaimer: I'm not 100% sure how codatatype works, especially when not referring to terminal algebras). Consider the "category of types", something like Hask but with whatever adjustment ...
2 votes
1 answer
124 views

What does the symbol `!` mean in type declarations in Haskell?

In my studies of Haskell, I see the symbol ! used in type declarations. See an example: data Foo = MkFoo { _bar :: !Bar , ... } My question is: why is it used and what is the difference to a ...
user avatar
0 votes
0 answers
22 views

Why does the java compiler need a seemingly useless wrapper function to type check the generic bounds? [duplicate]

class Test { static void foo(Class<?> clazz) { baz(clazz); // bar(clazz, clazz); <------- THIS LINE ERRORS OUT } static <T> void bar(Class<T> type, Class<? ...
  • 1,763
2 votes
2 answers
285 views

Is There Any Memory-Efficient Java Equivalent to C unions or C++ std::variant?

I have a class Element<T> that contains a T and an int: class Element<T>{ T obj; int i; // ... } When no T is stored, I would like to use obj like a pointer to an Element or ...
0 votes
3 answers
232 views

Is the TypeScript type system too relaxed in this case?

I think I've encountered a scenario that seems like it should cause the TS compiler to error (but it isn't) and I'm hoping someone can explain why. In the code below I'm passing an interface Foo to ...
  • 515
1 vote
0 answers
243 views

Typescript equivalent to C#'s NotNullWhen

When using non-nullable reference types in C# you can annotate an input parameter to show that it isn't null, when the method returns false: // From string bool IsNullOrEmpty([NotNullWhen(false)] ...
5 votes
1 answer
149 views

Are function parameters not polymorphic in Algorithm W (or Haskell)?

I am implementing Algorithm W for a toy language. I came across a case that I imagined would type check, but doesn't. I tried the same in Haskell, and to my surprise it didn't work there either. > (...
  • 18.4k
3 votes
3 answers
731 views

How to force a compile error in C++(17) if a function return value isn't checked? Ideally through the type system

We are writing safety-critical code and I'd like a stronger way than [[nodiscard]] to ensure that checking of function return values is caught by the compiler. [Update] Thanks for all the discussion ...
  • 302
2 votes
1 answer
235 views

How type declarations in brackets work in Haskell like (Integer -> Integer) -> Integer

I am a beginner at Haskell and programming. I am learning how to write functions based on type declarations.How to write function which types are declared in brackets like (a -> b) -> b. When I ...
  • 37
-1 votes
2 answers
83 views

Types should be the same but are not

I am not sure I understand why the first test evaluates to true and the second to false. I know that the information from typeid().name() is usually not reliable, but my main problem is with the ...
  • 23
7 votes
1 answer
206 views

What does coherence mean?

In the paper "Type classes: exploring the design space" by Simon Peyton Jones, Mark Jones and Erik Meijer, they define coherence informally as follows: Every different valid typing ...
  • 8,463
0 votes
0 answers
51 views

Why instance_size is 0 for fundamental GType types?

There are a bunch of fundamental types being registered in GLib's GType subsystem (GLib's source file gvaluetypes.c follows): /* --- type initialization --- */ void _g_value_types_init (void) { ...
  • 349
4 votes
3 answers
79 views

Is it common to have example values for compile-time checking and where should they go in the code?

I have a reasonably complex structure of data types and records, which is not so easy to make sense of by just looking at production code for someone not familiar with the codebase. To make sense of ...
  • 20.9k
0 votes
1 answer
101 views

How to exclude nonsensical types without relying on type inference?

I've been working on a type validator for Javascript to enable gradual typing for a language that was originally designed for dynamic types. Type validation means there is only type checking of terms ...
user avatar
2 votes
1 answer
118 views

How to reproduce GHC's type error for a rigid type variable escaping its scope?

Here is the canonical example for a rigid type variable escaping its scope: {-# LANGUAGE RankNTypes #-} runST :: forall a. (forall s. ST s a) -> a runST _ = undefined newRef :: forall s a. a -> ...
user avatar
1 vote
1 answer
289 views

How to constrain a type field to a power of two in a type system? [duplicate]

There is this in some JavaScript code: function allocate(bits) { if ((bits & (bits - 1)) != 0) { throw "Parameter is not a power of 2"; } ... } Essentially, there is a ...
  • 73.9k
2 votes
0 answers
107 views

Can typescript's discriminated union work with conditional types?

Suppose I have the following 3 types: type Apple = { type: "apple" } type Banana = { type: "banana" } type Fruit<T extends "apple" | "banana"> = T ...
0 votes
2 answers
194 views

Why is usage of the (erased) generic type in right-hand side allowed during type casting in Java?

This is disallowed, which I believe is due to type erasure. (T is erased and cannot be accessed in runtime to read its class like T.class). class Cup<T> { private T t; public T[] ...
  • 1,763
0 votes
0 answers
55 views

Hindley-Milner - conditional Substitutions?

I have been trying to build a type system with the Hindley-Milner Algorithm and ran into the following challenge and was curious if there are any resources or papers out there I can take a look at. ...
0 votes
0 answers
63 views

Generalised letrec semantics for mutual recursion

I'm new to system types and I was wondering how mutual recursion is defined through generalized let rec x1=e1 ,....,xn=en in e .What has to be added in the "simple" letrec's semantics and ...
0 votes
1 answer
112 views

When did C# get this "SFINAE-like" overload resolution of Action<..> parameters, and what is it called?

Consider the following code, where C# can disambiguate the overload based on the implicitly typed Action<T> that is supplied, where T is derived based on the [mutually exclusive] type-validity ...
  • 59.2k
1 vote
1 answer
52 views

How to use distinguish differenct object type in TypeScript?

How to distinguish different object type in TypeScript? interface CC { a: number; b: string } interface B { c:number } const obj: CC | B = { a: 1, c: 1 } // valid I want the ...
0 votes
1 answer
61 views

Typing a function with an interface of type in flowjs?

I have had quite a few look at the flow documentation, with some question still in mind. I have write a constructor named Track ;with my best attempt to type annotate it still not fully understanding ...
19 votes
5 answers
934 views

Can I print in Haskell the type of a polymorphic function as it would become if I passed to it an entity of a concrete type?

Here's a function polymorphic in 3 types: :t (.) (.) :: (b -> c) -> (a -> b) -> a -> c and here a non polymorphic function: :t Data.Char.digitToInt Data.Char.digitToInt :: Char -> ...
  • 21.8k
0 votes
1 answer
77 views

How to figure out the type if it is ambiguous type?

I am a Haskell beginner and I am having some trouble understanding this. I have 2 functions defined in a file like this: expr n x = (x ^ n)/(fact n) fact n | n == 0 = 1 | otherwise = n * fact (n -...
  • 979
0 votes
2 answers
182 views

Implications of automatic casting with double on dart/flutter

What are the implications of using an int were a double is required? dart allows you to declare a double without the .0 if it is 0 and handle that as a double without any kind of runtime casting? ...

1
2 3 4 5
10