archives

Abstractly typed languages

This is an admittedly rather vague idea that has occurred to me a few times - I'm wondering if anyone has had the same idea, or been able to formalize it in an interesting way.

I'm wondering if it would be possible to have a purely functional language, like Haskell, in which 'everything is an abstract data type'. There are no concrete data types in the language itself, everything is dealt with in an abstract / categorical / 'up to isomorphism' kind of way.

Data types would be chosen just to reflect what the data logically is, without concern for the physical representation or the performance characteristics of the algorithms involved. So a list of pairs, a hash-table and a function would all be of type Map. (or (Map a) => a, to borrow Haskell's typeclass notation)

The compiler, then, could chose which concrete implementation to use, say for a list or a map, based on any kind of compile-time or runtime optimizations it feels like. It can also apply lots of highly abstract categorically-based rewrite rules before it even gets to that stage.

Is this idea fatally flawed (I fear it might be, but I can't quite figure out how), or has anyone done anything similar?