Wednesday, March 4, 2009

Coalgebraic Comparison

If you lax some restrictions on types, you can describe some nice new types like coalgebraic lazy lists. Coalgebraic since it approximates the coalgebraic carrier type, and lazy since an extra construct is introduced which acts like the 'step'-function on a coalgebraic structure.

Below, an example.

import "system.hi"

namespace colist (

    using system
    using opt

    type colist = \=> unit -> opt (a, colist a)

    def conil: colist a = [ _ -> nothing ]

    def cocons: a -> colist a -> colist a =
        [ x, xx -> [ _ -> opt.just (x, xx) ] ]

    def cocat: colist a -> colist a -> colist a =
        [ xx, yy ->
            [ u ->
                v = xx u;
                if opt.nothing_test v then yy u
                    (x, xx) = opt.value v;
                    opt.just (x, cocat xx yy) ] ]

   def cocompare: ::Ord a => colist a -> colist a -> int =
        [ xx, yy ->
            v0 = xx nop;
            v1 = yy nop;
            if opt.nothing_test v0 then
                if opt.nothing_test v1 then 0 else 1
            else if opt.nothing_test v1 then (- 1)
                (x, xx) = opt.value v0;
                (y, yy) = opt.value v1;
                if x < y then (- 1)
                else if y < x then 1
                else cocompare xx yy ]

    def coprint: colist int -> unit =
        [ xx ->
            v0 = xx nop;
            if opt.nothing_test v0 then
                print "nil"
                (x, xx) = opt.value v0;
                _ = print (x+0);
                _ = print ", ";
                _ = coprint xx; 
                nop ]


using system
using colist

type tree = \=> [ leaf | branch (tree a) a (tree a) ]

def tree_to_colist: tree a -> colist a =
    [ leaf -> conil
    | branch l v r ->
        [ u ->
            cocat (tree_to_colist l) 
               (cocons v (tree_to_colist r)) u ] ]


  1. Why aren't you able to get your tree_to_colist function down to O(n) by using an "accumulator" to track your continuations:

    def tree_to_colist: tree a -> colist a -> colist a =
    [ leaf, xs -> xs
    | branch l v r, xs -> tree_to_colist l (cocons v (tree_to_colist r xs)) ]

    I'm also not quite clear why you need an eta-abstraction in the second case... but it's quite possible I'm missing something here.

    And, I'll admit your syntax does look to be rather clean, and probably an improvement on other ML dialects and Haskell... but you might want to consider tweaking your lexical syntax to allow hyphenated-identifiers, which I find much more humane than ugly_underscores or camelCase.

    Take care!

  2. I didn't think it over very well. And, actually, at the moment it is a really long time ago. Most of the extra eta's I introduced to mimic lazy semantics in an eager language, i.e. evaluation is deferred until an argument -usually unit- is supplied.

    Hyphenated identifiers? Uh, 'x-y'? No.