1
$\begingroup$

I'm fairly new to type systems and theory, so I would appreciate some guidance in a problem that sparked my interest.

I would like to understand what type system features are required so a compiler can enforce that a given key will return a value of the same type as the one the key was associated with in the first place.

A practical version of my problem is to declare a Map in TypeScript that allows a developer experience like in the pseudocode below:

const cache =  new  Map<K,  V>()

cache.set('Foo',  Error('R'))

cache.set('Bar',  1)

cache.get('Foo')  // Return value typed as Error.
  
cache.get('Bar')  // Return value typed as number.

cache.get('Qux')  // Compilation error.

What would the type of K and V be?

$\endgroup$
1
  • $\begingroup$ You can't do it like this. That said, why not just use statically typed variables Foo, Bar? Anything beyond that scenario is probably undecidable: if (undecidable condition) { cache.set('A', 1) } else { cache.set('A', 'B') } - and we don't know what type of A's value should be. $\endgroup$
    – user114966
    Aug 8 '20 at 15:36
2
$\begingroup$

What happens if I try to get Bar before it has been set? If you expect a compilation error, then you are not talking about a single type, but instead a sequence of types, where the type changes after each call to the set method. Look into 'strong update' and 'linear types'.

Why not just use a record type?

type MyRecord = { Foo : Error, Bar : number }
$\endgroup$
3
  • $\begingroup$ Thanks for taking a look. Could you elaborate on your suggestion of using a record type. The keys are not guaranteed to be just those 2. The keys should be understood as being of any type, but could be constrained to something sensible like any string. I apologize if my question was not clear. Let me know if it should be edited. $\endgroup$ Aug 11 '20 at 1:09
  • $\begingroup$ When people want this sort of thing, they are usually trying to initialize a set of typed fields one field at a time. But that is only superficially different from initializing them ``all at once'' as a record. Suppose we define a function whose parameter has your type. (x : YourType) => { return x.get("Bar") } $\endgroup$ Aug 12 '20 at 3:43
  • $\begingroup$ What is the function's return type? We can create multiple caches and set "Bar" to values of multiple different types. We can then pass these caches into the above function. In each case it will return a value of a different type, but a function must have one return type. That's why what you are talking about is not actually a type at all. $\endgroup$ Aug 12 '20 at 3:50
0
$\begingroup$

Existential types will do the trick.

Your question is not clear on this point, but as far as I can tell the keys are intended to be strings, and the values can have any type.

The type of cache.get is string → ∃ t . t, i.e., a function taking a string and return a results of type t, for some type t.

The type of cache.set is ∀ t . string → t → unit.

$\endgroup$
2
  • $\begingroup$ Does this "enforce that a given key will return a value of the same type as the one the key was associated with in the first place"? It doesn't seem like it, as there is nothing connecting the type of the argument to cache.set with the type of the result of cache.get. $\endgroup$
    – D.W.
    Aug 10 '20 at 2:18
  • $\begingroup$ That depends on the implementation. You could implement a cache which always returns 42. To enforce that the cache works correctly, you need a more expressive formalism, such as dependent types or a specification language. Once you have that it's pretty much the same thing to say "it returns the value that was put in" and "it returns a value of the same type that was put it". In any case, the whole thing is of ill-concived design and one should not be implementing cache this way, but I'd rather not get into a religuous war over this issue. $\endgroup$ Aug 11 '20 at 16:43

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.