[Haskell-cafe] Re: Heterogeneous Data Structures - Nested Pairs and functional references

[Heinrich Apfelmus]

Günther Schmidt wrote:
> I've been thinking a lot lately about heterogeneous and extensible data
> structures for which HList certainly offers a solution.
> 
> While HList is implemented through type-level programming I wonder if I
> can achieve similar results through value-level programming alone.
> 
> This is where I was thinking of functional references.
> 
> I wonder if or rather how one could do this:
> 
> Let's say there was some clever monad ...
> 
> someMonad = do
>     h1 <- add "twenty"
>     h2 <- add False
>     h3 <- add 16
>     .....   
>     modify h2 True
> 
> and get a ("twenty",(True, 16)) back. And while *in* the monad some
> accessors available.
> 
> Now come to think of it I think I actually read about this somewhere so
> I doubt this is truly my idea.
> 
> Anybody got some thoughts on this?

Dropping the part involving modification, I think you want to write
something like this

    val "twenty" `pair` (val False `pair` left)

where  left  is a "magic function" that returns the previous entry of
the pair, so that the whole expression yields

    ("twenty", (False, False))


The difficult part is to keep track of the types. But fortunately, there
is a neat trick by Oliver Danvy which does exactly that, see also

  Oliver Danvy. Functional unparsing.
  http://www.brics.dk/RS/98/12/BRICS-RS-98-12.pdf


Namely, let's assume we are already given a "magic" type constructor  |-
 (so magic that it's not even legal Haskell syntax) with the property that

    A |- B

somehow denotes an expression of type  B  with free variables of type  A
. In other words, the result of type  B  is somehow allowed to depend on
values of type  A .

Given this type, we can now assign types to our functions:

   pair :: (a |- b) -> ((a,b) |- c) -> (a |- (b,c))
   left :: (a,b) |- b
   val  :: x -> (a |- x)

In other words, everything may depend on additional free variables of
some type  a .

But of course,  A |- B  is just the same as  A -> B , which readily
suggest the implementation

    pair f g = \a -> let b = f a in (b, g (a,b))
    left     = \(a,b) -> b
    val x    = \a -> x

For instance, we get

    example :: a -> (String, (Bool, Bool))
    example = val "twenty" `pair` (val True `pair` left)

and

    example undefined = ("twenty",(True,True))


While the functionality is a bit limited, I'm confident that this
approach can be extended considerably. Whether the result is useful is
another question, of course.


Regards,
Heinrich Apfelmus

--
http://apfelmus.nfshost.com