Questions tagged [type-systems]
Type systems impose constraints on what programs may be written, by providing a syntactic method for operating with those constraints.
489
questions
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?
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 ...
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 ...
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 {
...
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 ...
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&...
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?
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 ...
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 ...
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 ...
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
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, ...
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 ...
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" ...
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 ...
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: ...
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<...>::...
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
...
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 = ' ' | ' '
...
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 ...
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<? ...
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 ...
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.
> (...
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 ...
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 ...
-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 ...
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 ...
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)
{
...
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 ...
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 ...
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 -> ...
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 ...
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[] ...
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 ...
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 -> ...
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 -...
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?
...