Take the 2-minute tour ×
Programmers Stack Exchange is a question and answer site for professional programmers interested in conceptual questions about software development. It's 100% free, no registration required.

If data is simple and objects are complex, I'm curious if there are any existing statically typed languages that would be able to augment(?) a map type into a type with guaranteed fields. I realize that at runtime, in any language this type of check is pretty doable. But in theory I also believe this should be possible to check with a compiler. To do everything below in Java, would be an explosion of interfaces (HasComplete, HasTitle, HasTitleAndComplete)

So has anyone done it? If not, how come? If so, how was it implemented?

This would allow you to read in data but then manipulate it with at least some type safety:

// User input is often simply converted to a Map
function parse(json) -> Map {...} 

// result still has all user input fields, 
// but this would be a runtime exception 
// if specified fields are missing
function cast(Map, Map<fields...>) -> Map<fields...> { ... }

input = "{title:'do it', complete: false, rank: 5, subtitle: 'now'}"

// Would throw class cast exception if complete or title were missing
todo = cast(parse(input), Map<title:str, complete:bool>)     

// Runtime introspection
todo instanceOf Map -> true
todo instanceOf Map<title:str, complete:bool> -> true
todo instanceOf Map<title:str> -> true
todo instanceOf Map<complete:bool> -> true
todo instanceOf Map<complete:date> -> false
todo instanceOf Map<rank:int> -> false because cast() did not specify rank
todo instanceOf Map<title:str, complete:bool, author:str> -> false 

// Typed methods based on map with certain fields
function capitalize_title(Map<title:str>) {...}
function finish_task(Map<complete:bool>) {...}
function finish_and_rename(Map<title:str, complete:bool>, newTitle) {...}
function increase_rank(Map<rank:int>) {...}

// Static Check compile pass
todo = capitalize_title(todo)
todo = finish_task(todo)
todo = finish_and_rename(todo, "[complete]")

// Static Check Compile Fail because cast() did not specify rank
increase_rank(todo)

// Methods could return a type with added (or removed) fields
function add_uuid(Map) -> Map<+id:int> {...}
todo_with_id = add_uuid(todo)
todo_with_id instanceOf Map<title:str, complete:bool, id:int> // true
share|improve this question
add comment

2 Answers

up vote 5 down vote accepted

There are so called dependently typed languages (Agda, Coq ...). These are very powerful and allow you to express a lot of information in the type system. Classical example is the type for a sorted list, allowing functions like (in imaginary concrete syntax):

sort :: List of a -> Sorted List of a

Of course this means that you have to convince your compiler, that your sorting algorithm is correct (and terminates) and you have to define what sorted means.

Somewhat less is expressible in languages like Haskell (maybe Scala, if you're looking for JVM executable language). You can define a type of list including that length of the list in the type. An obvious application is writing a function retrieving the first element of a list that cannot be accidentally called with an empty list. However, this is not what Haskell is intended for and comes with a price. Usually the drawbacks (mind boggling higher order type definitions and so on) outweigh the benefits if the language is not designed to handle these things.

This extends to maps. But parsing JSON data still might produce maps that are not defined for the fields you wish. There is no control over IO for the compiler/type checker. Thus you would either have to come up with default values or change the parse function type to result in an optional value, efficiently making it a partial function. Then you would have to disambiguate on this result (the compiler would force you to - good thing). But this is not so different from defining a type in a classic system (e.g. Java) that by contract requires the fields to be present and checks for this at runtime. The classical version is of course not as modular, you have seen that yourself.

share|improve this answer
    
This is exactly the answer I was hoping for, thank you. –  case nelson Apr 26 '12 at 12:46
1  
Now with the term in hand, I found this to be a good article on the subject axisofeval.blogspot.ca/2010/10/notes-on-dependent-types.html –  case nelson Apr 26 '12 at 13:12
add comment

In theory, an object is just a type-checked, static map, which means any OOP language offers a kind of static checking for map fields. However, I think what you're asking for is impossible.

Your code sample is, in brief, 1. Deserialize JSON into a map 2. Statically verify that the map is "proper". Since you can't deserialize JSON until you are running, you can't verify its structure until runtime. Even if you runtime create an object (or even a "strongly-typed map") using reflection, you are still verifying it at runtime.

A more practical approach to this than dependent typing (not that DT isn't practical or awesome, just not much support for it yet) might be code generation though templates of some kind. Most ORMs do something like this. They read in a schema from a database, then generate objects based on that schema. The same could be applied to arbitrary JSON to generate objects prior to compilation.

share|improve this answer
1  
No not quite, I realize that the initial user input may be incomplete and therefore any static analysis on it is impossible, however using a cast as in the example or a Maybe as scarfridge suggests would allow the static checker to reason about the program from that point forward. This way you can describe what you expect from input on the edge, verify that it satisfies that expectation, and then compose the rest of your program with guarantees that if you are dealing with a dependent type, then those fields or values will be present. –  case nelson Apr 27 '12 at 1:49
add comment

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

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