[<<][meta][>>][..]
Fri Oct 28 09:35:28 EDT 2011

Fixing type infrerence

No instance for (LoopFun Identity Value Tint Tint (r1 t1))

t17 = _app t16 (lit 2) :: I


Maybe the class def is a bit too general.  Here with fundeps removed
as they seem to not work.

class LoopFun m r t as ras where
  _lambda :: (ras -> m (r t)) -> r (as -> m t)
  _app :: r (as -> m t) -> (ras -> m (r t))


What I know is that ras has the forms:
 ()
 (r a, ())
 (r a, (r b, ()))

Which brings me straight back again to implementing tuples, which I
was trying to avoid because I couldn't figure it out.

Going in circles.

At this point however it does seem to be better to just focus on
argument lists.  The functions are unary, so really the only thing
that changes is those lists.

Now it's time to focus.  This is wrong:

  _app :: LoopArgs r as ras => r (as -> m t) -> ras -> m (r t)

  _app (Value f) (Value v) = 
    liftM Value $ f v  

/home/tom/meta/dspm/Loop.hs:152:19:
    Could not deduce (ras ~ Value as)
    from the context (LoopArgs Value as ras)
      bound by the type signature for
                 _app :: LoopArgs Value as ras =>
                         Value (as -> Identity t) -> ras -> Identity (Value t)
      at /home/tom/meta/dspm/Loop.hs:(152,3)-(153,21)
      `ras' is a rigid type variable bound by
            the type signature for
              _app :: LoopArgs Value as ras =>
                      Value (as -> Identity t) -> ras -> Identity (Value t)
            at /home/tom/meta/dspm/Loop.hs:152:3
    In the pattern: Value v
    In an equation for `_app':
        _app (Value f) (Value v) = liftM Value $ f v
    In the instance declaration for `Loop Identity Value'

Why?  
f :: as -> m t
but ras van't be unified with Value as
This is because we're not usng the LoopArgs op that does the conversion.

So we need to make sure that ras becomes r as using argsPack :: ras -> r as

What about this:

  _app f v = app f (argsPack v) where
    app (Value f) (Value as) = 
      liftM Value $ f as
      
It seems to compile.

But the type is probably wrong (flipped).
I need some terminology.

Let's use:

   rf  :: r (as -> m t)         representation of function
   hf  :: ras -> m (r t)        metalanguage HOS embedding

Funny how getting this commutation right is so confusing, but really
the whole point as it links 2 worlds: syntax objects and their
embedding as functions in a host language.

  argsPack   :: ras -> r as
  argsUnpack :: r as -> ras


In this way, _app will always act on (ra, (rb, ...)) == ras and not on
r (a,(b,...)) == r as so the types are correct:

  _lambda :: LoopArgs r as ras => (ras -> m (r t)) -> r (as -> m t)
  _app    :: LoopArgs r as ras => r (as -> m t) -> ras -> m (r t)

So the following typechecks,

  _lambda f = Value rf where
    rf as = do
      Value as <- f $ argsUnpack $ Value as
      return as

but I don't get why the (argsUnpack . Value) is necessary.  It seems
to be to make sure the representation type of functions is r (as -> m
t) and not r (ras -> r (m t)).  This seems rather arbitrary, though it
makes sense.

Next problems: 

- how to map ras to a list of variables?  This is needed in _app / App
  for Code.

- test if Value works now: make some recursive classes.




[Reply][About]
[<<][meta][>>][..]