[Haskell-cafe] Type-level programming [The container problem]

[Brandon S. Allbery KF8NH]

On 2008 Sep 28, at 4:47, Andrew Coppin wrote:
> By the way... I've seen a lot of type-level programs that allow you  
> to express (and therefore verify) some pretty extreme properties of  
> your code. In other words, you can make the compiler do more  
> checking than it normally would. But the actual compiled code  
> (assuming it does indeed compile) works exactly the same way as  
> before. Is there any way to use type-level programming to actually  
> alter the behaviour of the program in a useful/interesting way?


Aren't phantom types an example of this?  Absent the phantoms the  
program would (if it worked at all) treat expressions the same that it  
treats differently with them.

-- 
brandon s. allbery [solaris,freebsd,perl,pugs,haskell] allbery at kf8nh.com
system administrator [openafs,heimdal,too many hats] allbery at ece.cmu.edu
electrical and computer engineering, carnegie mellon university    KF8NH