[Haskell-cafe] Some thoughts on Type-Directed Name Resolution

[Paul R]

Steve> Every programmer has their own favorite editor, usually using the same
Steve> one to work in many different languages. For the moment, you'd have
Steve> a hard job separating me from Notepad++.

Main editors have very advanced customization features (though
incredibly hacky most of the time). A type-directed (this word is what
I like most in the proposal ;]) Haskell editing mode for them could be
a good first step.

Steve> If you really want a "semantic editor", I'd argue a rich visual
Steve> language with a file format that isn't intended to be read directly.
Steve> Something more like writing in Word than writing in TeX. But I don't
Steve> think most programmers are ready for this, for various reasons.
Steve> Version control tools and readable differences get a place near the
Steve> top of that list.

Well, in the long term I don't know ... maybe plain text won't be a good
representation of a program anymore. But in the short term that's not an
option. However, I see no problem in just constructing this textual
representation through a strictly type-directed (yeah!) syntax tree
editor.

Emacs, Vim, and a lot of others have "snippet" support. The workflow
could be something like :

  - action to create a new top-level function

  - PROMPT : name  (eg. map)
  - PROMPT : signature  (eg.  (a -> b) -> [a] -> [b])
  - PROMPT : parameters matching (eg. f (x:xs))

  - a stub is inserted with name, signature, and "undefined" definition
      map :: (a -> b) -> [a] -> [b]
      map f (x:xs) = undefined
      map f [] = undefined

  - now enters definition construction. You would start by adding to
    a 'pool' the bindings you want to combine. Some could be added to
    the pool automatically (function parameters, top-level definitions
    in the module, explicitly imported functions ...). Then you would
    pick one of them, and the type-directed system would offer
    type-correct completion. For example :

      - The pool state is { f :: a -> b , x :: a, xs :: [a], 
                            map :: (a -> b) -> [a] -> [b] }
        (the type variables scope over the entire pool)

      - The definition type must be [b]

      - I ask to use 'f'. It isn't [b] so I can't use it alone. The
        wonderful system would then reduce the pool to things that I can
        combine f with in order to keep the target [b] type. The result
        is { map f xs :: [b] }. I say ok.

      - The sub is now :
          map :: (a -> b) -> [a] -> [b]
          map f (x:xs) = map f xs
          map f [] = undefined

      - Now I ask to use (:) :: c -> [c] -> [c] . They are plenty of
        places where it could be used in the definition, so let's narrow
        the choice by associating the 'c' type to something in our
        expression : c == b. So (:) :: b -> [b] -> [b]

      - we have no expression typing as 'b' in the definition, but we
        have a single expression that types as [b], and it is 'map
        f xs'. So the system can safely offer :
          map :: (a -> b) -> [a] -> [b]
          map f (x:xs) = undefined : map f xs
          map f [] = undefined

      - now let's define the first 'undefined'. Its type is b. We ask
        this time to use the 'x' binding (x :: a). But we are looking
        for a 'b'. We have f :: a -> b so the system can offer 'f x'.

          map :: (a -> b) -> [a] -> [b]
          map f (x:xs) = f x : map f xs
          map f [] = undefined

      - The last undefined is trivial.


The user interface would certainly matter much, to have a fast and
pleasant experience. But the point is that as a pure language, haskell
very looks well suited for this kind of incremental syntax-tree editing,
with type-directed assistance. I wonder, even, if some rules could be
defined to construct automatically a definition that typechecks and use
all bindings in the pool :)

Back to the point of the thread, it looks like we certainly can target
type-directed editing with current haskell function notation, which has
the advantage of being beautiful and consistent.

-- 
  Paul