Questions tagged [type-systems]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
4
votes
1answer
127 views

Complexity of type-checking in relation to complexity of normalization

In order to verify that a terminating program terminates, one thing that can be done is to actually run the program. That may take a lot of time. If the program is typed in a total type-system, we can ...
4
votes
1answer
404 views

Featherweight Generic Java formalization in Coq

I've been searching for some nice formalization of FGJ (Featherweight Generic Java) in Coq. I am going to develop an extension of FGJ in Coq, so I hope there is an appropriate Coq implementation which ...
4
votes
1answer
121 views

Rendering of type-level computation

Programming languages with dependent types and/or higher-kinded types feature what might be called compile-time computation at the type-level. This is usually defined as follows (I'm omitting some ...
4
votes
0answers
61 views

Finite intersection property of polymorphic type families

Let $\Phi$ be a type functor definable in polymorphic lambda calculus: $$ \alpha : * \vdash \Phi(\alpha) : * $$ $$ f : A \to B \vdash \mathsf{Map}^{A,B}_\Phi(f) : \Phi(A) \to \Phi(B)$$ Suppose further ...
4
votes
0answers
77 views

Non-objected oriented type theories that can express the $\nu Obj$ calculus

Odersky et al.'s $\nu Obj$ calculus [1] adds just enough dependent typeness on top of object oriented programming to express interfaces that define types (and consequently module systems and other ...
4
votes
0answers
190 views

Type-and-effect systems, stochasticism and effect squelching: how about quicksort?

There's a feature of Haskell's type system which bugs me: you can't implement a randomized sorting algorithm without the use of randomness spilling out into all of its callers. That seems undesirable....
3
votes
1answer
125 views

Is there a 'very fast growing' hierarchy that would capture System F?

Particular ordinals in slow-growing and fast growing hierarchies can capture the expressiveness of many predicative type systems. Is there a hierarchy of function that could possibly capture ...
3
votes
1answer
502 views

Occurs check in type inference

I'm reading about type inference in chapter 30 of Programming Languages: Application and Interpretation and I'm trying to understand exactly how the occurs check works in an example I came up with. ...
3
votes
1answer
410 views

Language with extensible type system?

Is there a practical programming language that has an extensible type system? Or alternatively, an add-on type system that can be used with existing languages? With extensible I mean that the typing ...
3
votes
0answers
81 views

Is System-F with higher-kinded newtypes equivalent in computational power to System-F omega?

If we have System-F with higher-kinded types and newtypes, then we can express everything (I think) of System-F omega, except we have to manually (un)pack. For example: ...
2
votes
1answer
106 views

Is there a formalization of normalization of impredicative system F?

In particular Agda seems not strong enough to prove that. Is the predicative Calculus of Inductive Constructions universes (Coq without Prop) sufficient? How about with the impredicative Prop?
2
votes
1answer
214 views

programming language with type-level functions

Is there any programming language out there that allows the same set of tools it offers, to be used at the type level as well? I know, Haskell and some other ML family languages allow parametric types ...
2
votes
1answer
84 views

Completeness of Constraint Typing (type inference) question regarding $\sigma'$

The theorem of completeness of type inference states the following: Suppose $\Gamma \vdash t:S| _{\mathcal{X}}C$, ...
2
votes
1answer
197 views

Difference between statically and dynamically typed languages

When writing a course on computer science where students get an introduction to both Python and OCaml, I was on the verge of saying that Python is dynamically typed and OCaml is statically typed. I ...
1
vote
2answers
297 views

What are the limitations of dependent typing?

It seems dependent types can provide lots of desirable guarantees about program behavior. What kinds of program properties can they NOT guarantee (besides what's computationally infeasible)? Is there ...
1
vote
1answer
111 views

Type, operation and function, and their limits

First of all, sorry for my English. I would like to know, when I want to define a new type (I'm currently developing a computer interpreted language), how can I determine which "functions" are ...
1
vote
1answer
114 views

Dependent C-style types with subtyping rule

I'm looking for previous work regarding an extension of a C-style type system in which types may have constraints and have a defined subtyping rule. In particular, I'm interested in defining algebra-...
1
vote
0answers
46 views

Effect handlers, arrows and applicatives

After reading Lindley's paper on effect handlers for arrows and applicatives, I got the gist about dynamic and static flow and that it was added to the effect system and so on. However, I do not ...
1
vote
0answers
121 views

Has there been work on formal Semantics for linear algebra?

Could I get some references on formal semantics for a calculus on linear algebra that helps you study matrix or tensor based programming languages? I am looking for anything that encompasses linear or ...
0
votes
1answer
63 views

Is a reference on T a subtype of T?

If I take the book Practical Foundations for Programming Languages by Robert Harper, the following definition is given for subtyping: A subtype relation is a pre-order on types that validates the ...
0
votes
1answer
131 views

How to generalize a map of type for many operators?

I am formalizing the type system for a small language, and thus writing inference rules. Taking unary - operator for example, its entry may be a number as well as ...
0
votes
0answers
84 views

Semantics of a programming language [duplicate]

A newbie question, if I may... Could you be so kind and explain to me in plain english meaning of 'denotational semantics' and 'operational semantics'? I'm familiar with the definitions and have read ...
-3
votes
1answer
83 views

Soundness of type (systems)

For someone without strong background in theoretical computer science: can soundness be a property of a type (given a type system), or a property of type systems only? In other words, can we say that ...