RE: TypeFamilies vs. FunctionalDependencies type-level recursion

2011-06-17 Thread Simon Peyton-Jones
| I'd like to summarize the relationship between functional dependencies
| and type functions, and propose a solution that should get rid of
| overlapping instances. The solution does not require messing with
| System-FC. In fact, it can be implemented today (although
| ungainly). A small bit of GHC support will be appreciated.

This sounds good.  I am keen to identify features that provide the 
expressiveness that you and David and others want.  However my brain is small.

Concerning 1. mutual dependencies I believe that equality superclasses 
provide the desired expressiveness.  The code may not look quite as nice, but 
equality superclasses (unlike fundeps) will play nicely with GADTs, type 
families, etc. Do you agree?

Concerning 2. combination with overlapping instances, you say The solution 
has been described already in the HList paper: provide something the typeOf at 
the type level. That is, assume a type function TypeOf :: * - TYPEREP.  

By the HList paper do you mean http://homepages.cwi.nl/~ralf/HList/?  I see 
no TYPEREP in that paper.  Do you think you might perhaps elaborate your 
proposed solution explicitly?  Perhaps saying explicitly:
  - This is the support we need from GHC
  - This is how you can then code examples X,Y,Z

I know that all of this is embedded variously in your past writings but I'm not 
very good at finding exactly the right bits and turning them into proposed 
features!

Incidentally Pedro's new deriving Generic stuff does derive a kind of 
type-level type representation for types, I think.  It's more or less as 
described in their paper.
http://www.dreixel.net/research/pdf/gdmh_nocolor.pdf

Thanks

Simon


___
Haskell-prime mailing list
Haskell-prime@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-prime


Re: TypeFamilies vs. FunctionalDependencies type-level recursion

2011-06-17 Thread dm-list-haskell-prime
At Fri, 17 Jun 2011 13:21:41 +,
Simon Peyton-Jones wrote:
 
 Concerning 1. mutual dependencies I believe that equality
 superclasses provide the desired expressiveness.  The code may not
 look quite as nice, but equality superclasses (unlike fundeps) will
 play nicely with GADTs, type families, etc. Do you agree?

By equality superclasses, do you just mean being able to say a ~ b
in a class context?  If so, that is basically what you get by enabling
fundeps and defining a class such as:

class AssertEq a b | a - b, b - a
instance AssertEq a a

Unless I'm missing something, that is not sufficient to do a lot of
things I would like to do, as those things require both
OverlappingInstances and FunctionalDependencies (as well as
UndecidableInstances).  A good test would be whether superclasses let
you eliminate N^2 mtl instances and do something equivalent to:

instance (Monad m) = MonadState s (StateT s m) where
get   = StateT $ \s - return (s, s)
put s = StateT $ \_ - return ((), s)

instance (Monad (t m), MonadTrans t, MonadState s m) =
MonadState s (t m) where
get = lift get
put = lift . put

Superclass equality is crucial for type families, since you can't
mention a class's own type function in its head, but are there other
things they allow you do to?

 Concerning 2. combination with overlapping instances, you say The
 solution has been described already in the HList paper: provide
 something the typeOf at the type level. That is, assume a type
 function TypeOf :: * - TYPEREP.
 
 ...
 
 Incidentally Pedro's new deriving Generic stuff does derive a kind of 
 type-level type representation for types, I think.  It's more or less as 
 described in their paper.
 http://www.dreixel.net/research/pdf/gdmh_nocolor.pdf

I'm very excited about this new Representable class and have just
started playing with it, so it is too early for me to say for sure.
However, my initial impression is that this is going to make me want
OverlappingInstances even more because of all the cool things you can
do with recursive algorithms over the Rep types...

An initial issue I'm running into (and again, this is preliminary,
maybe I'll figure out a way without OverlappingInstances) is in
implementing a function to serialize Generic data types to JSON.  If
the Haskell data type has selectors (i.e., is a record), then I would
like to serialize/unserialize the type as a JSON object, where the
names of the selectors are the JSON field names.  If the Haskell data
type does not have selectors, then I would like to serialize it as a
JSON array.

Generic deriving gives me the conIsRecord function, but this is at the
value level, and I want to do something different at the type level.
For a record, I need a list of (String, Value) pairs, while for a
non-record, I need a list of Values.  This leads me to write code such
as the following:

 class JSON1 a r | a - r
 toJSON1 :: a - r

 instance (JSON a) = JSON1 (S1 NoSelector (K1 c a)) [Value] where
 toJSON1 (M1 (K1 a)) = [toJSON a]

 instance (Selector x, JSON a) = JSON1 (S1 x (K1 c a)) [(String, Value)] where
 toJSON1 s@(M1 (K1 a)) = [(nameOf s undefined, toJSON a)]
 where nameOf :: S1 c f p - c - String
   nameOf _ c - selName c

The key piece of magic I need here (and in so many other places) is to
be able to do one thing at the type level if x is a particular type
(e.g., NoSelector) or sometimes one of a small number of types, and to
do something else if x is any other type.

Closed type families might do it.  One question I should think about
is whether a combination of open type families with safe dynamic
loading (if this is possible) and closed type families would cover
everything I need.  You'd need to be able to do things like:

-- Type-level if-then-else
closed type family IfEq :: * - * - * - * - *
type instance IfEq a b c d = d
type instance IfEq a a c d = c

You would also need to be able to dangle closed type families off of
open ones.  (I.e., type instance Foo ProxyType = MyClosedTypeFamily)

I also can't quite figure out how to pass around ad-hoc polymorphic
functions the way you can with proxy types and a class such as:

class Function f a b | f a - b where funcall :: f - a - b

David

___
Haskell-prime mailing list
Haskell-prime@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-prime


RE: TypeFamilies vs. FunctionalDependencies type-level recursion

2011-06-17 Thread Simon Peyton-Jones
| By equality superclasses, do you just mean being able to say a ~ b
| in a class context? 

Yes.  Or (F a ~ b).

| Unless I'm missing something, that is not sufficient to do a lot of
| things I would like to do, as those things require both
| OverlappingInstances and FunctionalDependencies (as well as
| UndecidableInstances). 

Correct. Hence Oleg's second point 2. combination with overlapping instances.

Oleg claims to have a good story here.  I'd like to see how he uses it to solve 
your problem.

Simon

___
Haskell-prime mailing list
Haskell-prime@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-prime