[<<][meta][>>][..]
Fri Oct 28 11:34:27 EDT 2011

LoopArgs


{- Encodes the relation between a metalanguage tree of represented
   values and a representation of a tree value.  I.e.

          (r a, (r b, r c))   <->   r (a,(b,c))
-}
class LoopArgs r as ras | ras -> r, ras -> as where
  argsPack   :: ras -> r as
  argsUnpack :: r as -> ras


TODO: write the recursive instance.

Blank stare..

Something doesn't add up...  Maybe it's too simple?  What I need is a
way to distribute a simple constructor over tuples.  That really can't
be too hard, but to do it in a generic way the constructor and
destructor need to be wrapped.

Maybe this is the basic idea:

{- Constructor that commutes with binary tupling operator. -}
class Pair c where
  cons   :: (c a, c b) -> c (a, b)
  uncons :: c (a, b) -> (c a, c b)




How bout this as final solution?

{- Encodes the relation between a metalanguage tree of represented
   values and a representation of a tree value.  I.e.

          (r a, (r b, r c))   <->   r (a,(b,c))
-}
class Args r as ras | ras -> r, ras -> as where
  pack   :: ras -> r as
  unpack :: r as -> ras


{- Constructor supporting commute with binary tupling. -}
class Pair c where
  cons   :: (c a, c b) -> c (a, b)
  uncons :: c (a, b) -> (c a, c b)

instance (Pair r, Args r as r_as, Args r bs r_bs)
         => Args r (as,bs) (r_as, r_bs) where
  pack (r_as, r_bs) = cons (pack r_as, pack r_bs)
  unpack r_as_bs =  (unpack r_as, unpack r_bs) where
    (r_as, r_bs) = uncons r_as_bs

instance (Pair r, TMLprim t) => Args r t (r t) where  
  pack = id
  unpack = id


instance Pair Value where
  cons (Value a, Value b) = Value (a,b)
  uncons (Value (a, b)) = (Value a, Value b)
 

Then trouble:

f1 :: (Args r as ras, Loop m r) => r (as -> m t)
f1' :: Value (Tint -> Identity Tint)
f1' = f1

    No instance for (Args Value Tint ras0)
      arising from a use of `f1'
    Possible fix:
      add an instance declaration for (Args Value Tint ras0)
    In the expression: f1
    In an equation for `f1'': f1' = f1
Failed, modules loaded: StateCont, Term, TML, Compile, Loop.


It seems that the ras parameter is not fixed when specifying the type
of f1'.  Indeed, it does not appear in r (as -> m t).  So this needs
some functional dependency maybe?

This is called an "ambiguous type".  See [1]

What I want to express is that r and as together imply ras.  How to do
that?

What I need to do is to try to really understand functional
dependencies, and see how (or why not) I can have multi-arg fundeps.


Anyways, in the mean time I removed the fundeps from Args, and used an
explicit type signature:

  _app rf ras = app rf (pack ras) where
    app :: Code (as -> MCode t) -> Code as -> MCode (Code t)
    app (Code (FRef f)) (Code as) = 
      return $ Code $ App f [] -- FIXME: compile variables


After reading part of [1]: multi-arg deps are simple:  a b -> c
Does that solve it?

Almost.. I had to add some type annotation.  Especially the "forall as
ras t" seems to be significant.  To introduce type scoping?  I thought
it was implicit.

  _lambda = lambda where
    lambda :: forall as ras t. Args Value as ras => 
              (ras -> Identity (Value t)) -> Value (as -> Identity t)
    lambda f = Value rf where
      rf as = do
        Value t <- f  $ unpack $ Value (as :: as)
        return t


[1] http://www.reddit.com/r/haskell/comments/7oyg5/ask_haskellreddit_can_someone_explain_the_use_of/



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