Re: the MPTC Dilemma (please solve)

[Roman Leshchinskiy]

On Thu, 23 Mar 2006, Claus Reinke wrote:


  class Graph (g e v) where
  src :: e - g e v - v
  tgt :: e - g e v - v

  we associate edge and node types with a graph type by
  making them parameters, and extract them by matching.


If I understand correctly, this requires all graphs to be polymorphic in 
the types of edges and vertices. Thus, you cannot (easily) define a graph 
which provides, say, only boolean edges. Moreover, doesn't this require 
higher-order matching?


I've already answered the last question. as for polymorphism, all this
requires is for a graph type parameterized by an edge and vertex
type (just as the SML solution, which got full marks in this category,
requires instantiations of the edge and vertex types in the graph structure).


Ah, I see. You are suggesting to introduce phantom type parameters to fake 
polymorphism for types which aren't really polymorphic. This might be 
acceptable as a temporary workaround but I don't think it is a good 
long-term solution. The ML implementation is not really comparable to this 
as instantiating structures is quite different from instantiating types.



  class Edge g e | g - e
  instance Edge (g e v) e
  class Vertex g v | g - v
  instance Vertex (g e v) v

  class (Edge g e,Vertex g v) = Graph g where
  src :: e - g - v
  tgt :: e - g - v

  (this assumes scoped type variables; also, current GHC,
   contrary to its documentation, does not permit entirely 
FD-determined variables in superclass contexts)


This does not seem to be a real improvement to me and, in fact, seems quite 
counterintuitive.


it is, however, probably as close as we can come within current Haskell,


In what sense is this current Haskell? For this to work, you need at the 
very least to


  a) allow FD-determined variables to appear only in the superclass
 contexts but not in the head of class declarations (not supported by
 GHC at the moment),
  b) rely on scoped type variables (in a way which GHC doesn't support at
 the moment) and
  c) provide a way to keep FD outputs abstract even when the inputs are
 known (not supported by GHC).

While a) and b) might be fairly minor changes to GHC, c) seems to be a 
major one. Even if all this is added, what you end up with is essentially 
a verbose and counterintuitive hack for something which should be easy to 
do. This is not meant as a criticism of your (very interesting, IMO) 
approach - I agree that this is probably the best you can do with FDs. 
It's just that FDs simply seem to be a less than optimal mechanism for 
this kind of programming.


Also, it might be worth pointing out that even if all of the above worked,
you still couldn't do

  data VertexPair g = VP (Vertex g) (Vertex g)
  fstVertex :: Graph g = VertexPair g - Vertex g
  fstVertex (VP v1 v2) = v1

  type Vertices g = [Vertex g]

Roman

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

Re: the MPTC Dilemma (please solve)

[Roman Leshchinskiy]

On Thu, 23 Mar 2006, Claus Reinke wrote:

Ah, I see. You are suggesting to introduce phantom type parameters to fake 
polymorphism for types which aren't really polymorphic. This might be 
acceptable as a temporary workaround but I don't think it is a good 
long-term solution. The ML implementation is not really comparable to this 
as instantiating structures is quite different from instantiating types.


if we could actually write the instance implementations, it would be easier
to say whether this is an adequate approach. once the phantom types are 
connected to the actual types used in the implementation, I suspect this

would be very similar to the use of structure sharing and signature inclusion
in the ML implementation.


I would consider relying on any similarities between Haskell's data types 
and ML structures to be a bad thing, since the two are entirely different 
beasts. In particular, although the phantom types trick works to an 
extent, it is highly problematic from the software engineering point of 
view. Suppose I have a library which defines a monomorphic IntGraph type 
with specific vertex and edge types and does not know nor care about my 
Graph class. With your approach, I have to do something like


  data IntGraph' v e = IG IntGraph
  type MyIntGraph = IntGraph' Int (Int,Int)

declare all the instances and provide an impedance matching module which 
provides all IntGraph operations (which I want to use in addition to the 
Graph operations) for MyIntGraph. With ATs, I just have to do


  instance Graph IntGraph where
type Vertex IntGraph = Int
type Edge   IntGraph = (Int,Int)

ML structures are equally easy to use.


it is, however, probably as close as we can come within current Haskell,
In what sense is this current Haskell? 


ignoring accidental limitations in current implementations.


Are you sure that all these limitations really are accidential?

thanks. I'm not saying that ATS are a  bad thing, either, just that once we 
have a proper basis on which to rid current FD implemenations of accidental 
limitations, we should be able to implement ATS as a syntax transformation.


Even if it is possible to push FDs far enough to be able to translate ATs 
into them, why would you want to do so in the context of Haskell's 
development (it is certainly an interesting theoretical question, though)?
Having both mechanisms in one language doesn't seem to be a good idea to 
me and ATs seem to fit much better with the rest of Haskell and, 
consequently, are much easier to program with.



Also, it might be worth pointing out that even if all of the above worked,
you still couldn't do

  data VertexPair g = VP (Vertex g) (Vertex g)
  fstVertex :: Graph g = VertexPair g - Vertex g
  fstVertex (VP v1 v2) = v1

  fstVertex :: Graph g = VertexPair g - Vertex g
  fstVertex (VP v1 v2) = v1


a variation of problem (a) above: contexts can introduce new, FD-bound
variables only in type signatures at the moment, not in class or data 
declarations.


  data Vertex g v = VertexPair g v = VP v v
  fstVertex :: (Vertex g v, Graph g) = VertexPair g v - v
  fstVertex (VP v1 v2) = v1

otherwise, we could omit the spurious v parameter, as we'd like to.


I presume you are suggesting

  data Vertex g v = VertexPair g = VP v v

This would only affect the type of VP. Suppose we have

  rank :: (Vertex g v, Graph g) = g - v - Int

Presumably, we could then write

  rankFst :: Graph g = g - VertexPair g - Int
  rankFst g (VP v1 v2) = rank g v1

How does rankFst get the dictionary for Vertex g v which it must pass to 
rank (in a dictionary-based translation, at least)? It can be extracted 
from the Graph dictionary, but how does the compiler know?


Alternatively, we might try

  data VertexPair g = forall v . Vertex g v = VP v v

but now fstVertex doesn't work anymore (for reasons which, IIRC, are not 
accidential). These problems disappear with ATs (I think) as here, only 
the Graph dictionary is required by all operations.


Roman

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

Re: the MPTC Dilemma (please solve)

[Roman Leshchinskiy]

On Mon, 20 Mar 2006, Claus Reinke wrote:


variant A: I never understood why parameters of a class declaration
  are limited to variables. the instance parameters just have
  to match the class parameters, so let's assume we didn't
  have that variables-only restriction.

  class Graph (g e v) where
  src :: e - g e v - v
  tgt :: e - g e v - v

  we associate edge and node types with a graph type by
  making them parameters, and extract them by matching.


If I understand correctly, this requires all graphs to be polymorphic in 
the types of edges and vertices. Thus, you cannot (easily) define a graph 
which provides, say, only boolean edges. Moreover, doesn't this require 
higher-order matching?



variant B: I've often wanted type destructors as well as constructors.
  would there be any problem with that?

  type Edge (g e v) = e
  type Vertex (g e v) = v

  class Graph g where
  src :: Edge g - g - Vertex g
  tgt :: Edge g  - g - Vertex g


This suffers from the same problems as the previous variant. It also looks 
a lot like a special form of associated types. Could the AT framework be 
extended to support a similar form of type synonyms (in effect, partial 
type functions outside of classes)? Would


  instance Graph Int
-- methods left undefined

be a type error here?


variant C: the point the paper makes is not so much about the number
  of class parameters, but that the associations for concepts
  should not need to be repeated for every combined concept.
  and, indeed, they need not be

  class Edge g e | g - e
  instance Edge (g e v) e
  class Vertex g v | g - v
  instance Vertex (g e v) v

  class (Edge g e,Vertex g v) = Graph g where
  src :: e - g - v
  tgt :: e - g - v

  (this assumes scoped type variables; also, current GHC,
   contrary to its documentation, does not permit entirely 
FD-determined variables in superclass contexts)


What are the types of src and tgt here? Is it

  src, tgt :: (Edge g e, Vertex g v, Graph g) = e - g - v

This does not seem to be a real improvement to me and, in fact, seems 
quite counterintuitive.


Roman

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

Re: the MPTC Dilemma (please solve)

[Claus Reinke]

  class Graph (g e v) where
  src :: e - g e v - v
  tgt :: e - g e v - v

  we associate edge and node types with a graph type by
  making them parameters, and extract them by matching.


If I understand correctly, this requires all graphs to be polymorphic in 
the types of edges and vertices. Thus, you cannot (easily) define a graph 
which provides, say, only boolean edges. Moreover, doesn't this require 
higher-order matching?


I've already answered the last question. as for polymorphism, all this
requires is for a graph type parameterized by an edge and vertex
type (just as the SML solution, which got full marks in this category,
requires instantiations of the edge and vertex types in the graph structure). 
I already gave an example of a graph instantiated with (Int,Int) edges 
and Int vertices. see below for a translation of the ATC paper examples



variant B: I've often wanted type destructors as well as constructors.
  would there be any problem with that?

  type Edge (g e v) = e
  type Vertex (g e v) = v

  class Graph g where
  src :: Edge g - g - Vertex g
  tgt :: Edge g  - g - Vertex g


This suffers from the same problems as the previous variant. It also looks 
a lot like a special form of associated types. Could the AT framework be 
extended to support a similar form of type synonyms (in effect, partial 
type functions outside of classes)? 


it suffers as little as the previous variant. and it was meant to be a special
form, showing that the full generality of ATs as a separate type class 
extension is not required to solve that paper's issue. and the translation 
from type functions to FDs or ATs is entirely syntactic, I think, so it 
would be nice to have in Haskell', as long as at least one of the two is 
included.



Would

  instance Graph Int
-- methods left undefined

be a type error here?


yes, of course. instances still have to be instances of classes. in variation
A, the type error would be in the instance head, in variation B, it would
be in the method types (although it could backpropagate to the head).


  class Edge g e | g - e
  instance Edge (g e v) e
  class Vertex g v | g - v
  instance Vertex (g e v) v

  class (Edge g e,Vertex g v) = Graph g where
  src :: e - g - v
  tgt :: e - g - v

  (this assumes scoped type variables; also, current GHC,
   contrary to its documentation, does not permit entirely 
FD-determined variables in superclass contexts)


What are the types of src and tgt here? Is it

  src, tgt :: (Edge g e, Vertex g v, Graph g) = e - g - v


yes.

This does not seem to be a real improvement to me and, in fact, seems 
quite counterintuitive.


Roman


you're free to your own opinions, of course!-)

it is, however, probably as close as we can come within current Haskell,
and the shifting of Edge/Vertex to the right of the '=' is a purely syntactic
transformation, even if it is a nice one.

and as you can see from the implementation below (I had to move the 
class methods out of the class to circumvent GHC's current typing problem, 
so no method implementations, only the types), it is sufficient to address the 
problem in that survey paper, and accounting for graphs with specific types 
is no problem (direct translation from ATC paper examples):


   *Main :t \e-src e (undefined::NbmGraph)
   \e-src e (undefined::NbmGraph) :: GE2 - GV2
   *Main :t \e-src e (undefined::AdjGraph)
   \e-src e (undefined::AdjGraph) :: GE1 - GV1

cheers,
claus

{-# OPTIONS_GHC -fglasgow-exts #-}

class Edge g e | g - e
instance Edge (g e v) e 


class Vertex g v | g - v
instance Vertex (g e v) v

class Graph g
-- these should be class methods of Graph..
src, tgt :: (Edge g e,Vertex g v,Graph g) = e - g - v
src = undefined
tgt = undefined

-- adjacency matrix
data G1 e v = G1 [[v]]
data GV1 = GV1 Int
data GE1 = GE1 GV1 GV1
type AdjGraph = G1 GE1 GV1  -- type associations

instance Graph AdjGraph

-- neighbor map
data FiniteMap a b
data G2 e v = G2 (FiniteMap v v) 
data GV2 = GV2 Int

data GE2 = GE2 GV2 GV2
type NbmGraph = G2 GE2 GV2  -- type associations

instance Graph NbmGraph

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

Re: the MPTC Dilemma (please solve)

[Claus Reinke]

you're right about interactions in general. but do you think constructor 
classes specifically would pose any interaction problems with FDs?

You have to be more careful with unification in a higher-kinded setting.
I am not sure how to do that with CHRs.


to quote from the ATS paper: just like Jones, we only need first-order
unification despite the presence of higher-kinded variables, as we require
all applications of associated type synonyms to be saturated.


variant A: I never understood why parameters of a class declaration
are limited to variables. the instance parameters just have
to match the class parameters, so let's assume we didn't
have that variables-only restriction.

class Graph (g e v) where
src :: e - g e v - v
tgt :: e - g e v - v

we associate edge and node types with a graph type by
making them parameters, and extract them by matching.


The dependency seems to be lost here.


what dependency?

the associated types have become parameters to the graph type,
so the dependency of association is represented by structural inclusion
(type constructors are really constructors, so even phantom types
would still be visible in the type construct). any instances of this class 
would have to be for types matching the form (g e v), fixing the type 
parameters.



variant B: I've often wanted type destructors as well as constructors.
would there be any problem with that?

type Edge (g e v) = e
type Vertex (g e v) = v

class Graph g where
src :: Edge g - g - Vertex g
tgt :: Edge g  - g - Vertex g


Also no dependency and you need higher-order matching, which in general
is undecidable.


the dependency is still represented by the type parameters, as in the
previous case. and is this any more higher-order than what we have 
with constructor classes anyway? here's an example implementation

of the two destructors, using type classes with constructor instances:

   {-# OPTIONS_GHC -fglasgow-exts #-}

   import Data.Typeable

   data Graph e v = Graph e v

   class Edge g e | g - e where edge :: g - String
   instance Typeable e = Edge (g e v) e where edge g = show (typeOf 
(undefined::e))

   class Vertex g v | g - v where vertex :: g - String
   instance Typeable v = Vertex (g e v) v where vertex g = show (typeOf 
(undefined::v))

[the Typeable is only there so that we can see at the value level that 
the type-level selection works]


   *Main edge (Graph (1,1) 1)
   (Integer,Integer)
   *Main vertex (Graph (1,1) 1)
   Integer


variant C: the point the paper makes is not so much about the number
of class parameters, but that the associations for concepts
should not need to be repeated for every combined concept.
and, indeed, they need not be

class Edge g e | g - e
instance Edge (g e v) e
class Vertex g v | g - v
instance Vertex (g e v) v

class (Edge g e,Vertex g v) = Graph g where
src :: e - g - v
tgt :: e - g - v

(this assumes scoped type variables; also, current GHC,
 contrary to its documentation, does not permit entirely 
 FD-determined variables in superclass contexts)


You still need to get at the parameter somehow from a graph (for which
you need an associated type).


oh, please! are you even reading what I write? as should be clear from 
running the parts of the code that GHC does accept (see above), FDs

are quite capable of associating an edge type parameter with its graph.

all three seem to offer possible solutions to the problem posed in 
that paper, don't they?


Not really.


...


II. The other one is that if you use FDs to define type-indexed
types, you cannot make these abstract (ie, the representations
leak into user code).  For details, please see the Lack of
abstraction. subsubsection in Section 5 of
http://www.cse.unsw.edu.au/~chak/papers/#assoc

do they have to? if variant C above would not run into limitations
of current implementations, it would seem to extend to cover ATS:

class C a where
type CT a

instance C t0 where
type CT t0 = t1

would translate to something like:

class CT a t | a - t
instance CT t0 t1

class CT a t = CT a
instance CT t0 t1 = C t0

as Martin pointed out when I first suggested this on haskell-cafe,
this might lead to parallel recursions for classes C and their type
associations CT, so perhaps one might only want to use this to
hide the extra parameter from user code (similar to calling auxiliary
functions with an initial value for an accumulator).


That doesn't address that problem at all.


come again? CT expresses the type 

Re: the MPTC Dilemma (please solve)

[Claus Reinke]

welcome to the discussion!-)


(A) It's not as if every interesting program (or even the majority of
interesting programs) use(s) MPTCs.


well, I express my opinions and experience, and you express your's:-)

let's hope that Haskell' will accomodate both of us, and all the other
possible views and applications of Haskellers in general, to the extent 
that they are represented here.



(B) I don't think the time for which an extension has been around is
particularly relevant. 


oh yes, it is. don't get me wrong, we have ample proof that having 
been around for long does not imply good, necessary or even just 
well-understood. but it is certainly relevant, as it demonstrates

continued use.

haskell prime is an attempt to standardize current Haskell practice, 
and MPTCs and FDs have been part of that for a long time, so haskell
prime has to take a stand about them. Haskell98 could get away with 
closed eyes, claiming that those features were new then, just as GADTs 
and ATS are new today. haskell prime does not have that choice

any more.

so I see two choices:

- define current practice in MPTCs and FDs, then mark those then
   well-defined extensions as deprecated, to be removed in Haskell''.

   to do this, you'd need to provide a clear alternative to migrate to,
   with a simple and complete definition both of the feature set you
   are advocating, and its interactions with other features, and its
   relation to the features it is meant to replace.

- define current practice in MPTCs and FDs, find the simple story
   behind these features and their interactions with other features
   (as simple as we can make it, without the scaremongering), and 
   add that to Haskell'. 

   also define the initial versions of your alternative feature sets 
   and their interactions. leave it to Haskell'' to decide which of 
   the two to deprecate, if any.


either option needs a definition of both feature sets (I assume you're
arguing for associated type synonyms). we do have fairly simple
definitions of MPTCs and FDs, although I still think (and have been
trying to demonstrate) that the restrictions are too conservative. 

what we don't have are definitions of the interactions with other 
features (and the restrictions really get in the way here), such as 
overlap resolution, or termination proofs, but we are making 
progress there. what we also don't have is a simple definition 
of ATS, its interactions with other features, and a comparison 
of well-understood ATS with well-understood FDs (I only just 
printed the associated FD paper, perhaps that'll help), which 
could form the basis for a decision between the two.


so, imho, haskell prime can only define the current state, hopefully
with a better form of MPTCs/FDs and at least some preliminary 
form of ATS, and let practice over the next years decide whether 
haskellers will move from MPTCs/FDs to ATS. just as practice

seems to have decided that other features, eg, implicit parameters,
in spite of their initial popularity, have not recommended themselves
for any but the most careful and sparing use, and not as part of
the standard.


One of the big selling points of Haskell is that
it's quite well defined, and hence, its semantics is fairly well
understood and sane - sure, there are dark corners, but compared to
other languages of the same size, we are in good shape.  If we include
half-baked features, we weaken the standard.


we are not in a good shape. Haskell 98 doesn't even have a semantics.

current Haskell is so full of dark corners, odd restrictions and unexpected
feature interactions that I've been tempted to refer to it as the C++ of
functional languages. the question on the table is not wether to include
half-baked features of current Haskell in Haskell', but how to make sure
that we understand those features well enough to make an informed
decision. nothing I've seen so far indicates that it is impossible to come
up with a well-defined form of some of those features, including their 
interactions with other features. that doesn't come without some 
further work, so the haskell prime effort cannot just pick and choose,

but there's no reason to give up just yet.

and to keep what is good about Haskell, we need to think about
simplifying the features we have as our understanding of them improves,
in particular, we need to get rid of unnecessary restrictions (they
complicate the language), and we need to investigate feature interactions.
we weaken the standard if it has nothing to say about the problems
in current practice.


In fact, it's quite worrying that FDs have been around for so long and
still resisted a thorough understanding.


they don't resist. but as long as progress is example-driven and scary
stories about FDs supposedly being tricky and inherently non-under-
standable are more popular than investigations of the issues, there 
won't be much progress. please don't contribute to that hype.


you reply to a message that is about a month 

Re: the MPTC Dilemma (please solve)

[Ross Paterson]

On Mon, Mar 20, 2006 at 10:50:32AM -, Claus Reinke wrote:
 you reply to a message that is about a month old. since then, every
 single example of FD trickyness presented here has been resolved
 (or have we missed some example?), and as far as I'm concerned, 
 the remaining problems are due to feature interactions, and need a 
 more systematic approach.

As understand it, you've proposed changes in context reduction to
restore confluence:

http://www.haskell.org//pipermail/haskell-prime/2006-March/000880.html
(with subsequent minor corrections)

What is your plan to deal with non-termination (e.g. examples 6 and 16
of the FD-CHR paper)?

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

Re: the MPTC Dilemma (please solve)

[Claus Reinke]

As understand it, you've proposed changes in context reduction to
restore confluence:


yes.


What is your plan to deal with non-termination (e.g. examples 6 and 16
of the FD-CHR paper)?


I haven't read all the suggestions that Martin, you, and others have 
made in that area yet (still busy with overlaps), including those in the 
revised FD-CHR paper, so I can't make concrete suggestions yet, 
beyond those I've already posted here:


1 we all want terminating instance inference, but trying to assure that
   via restrictions is bound to be limiting (does GHC still have to build
   part of the hierarchical libs with -fallow-undecidable-instances?).

   I'm not opposed to it, but I'd like Haskell' to document current
   practice, in that we have the option to switch of termination checks
   whenever they are not able to see that our programs are terminating
   (available in Hugs and GHC, and all too often necessary).

2 that said, termination checks can do a lot, and it is certainly useful
   know various methods of checking terminations, as well as terminating
   examples beyond current termination checks.

   the old FD-CHR draft already discussed relaxed FD conditions,
   but was somewhat hampered because confluence checks seemed
   entangled with termination. with confluence problems out of the
   way, the restrictions can focus on termination. was there any other
   reason not to go for the relaxed FD conditions as a start?

3 in http://www.haskell.org//pipermail/haskell-prime/2006-February/000825.html

   I gave two examples that are terminating, but for which the
   current conditions are too restrictive. the first could be cured
   by taking smaller predicates into account, in addition to smaller
   types and smaller variable sets, and the second turned out to be 
   a special case of the relaxed coverage condition, I think. I run 
   into both problems all the time (the first is especially annoying as 
   it prevents calling out to simpler helper predicates..).


4 example 6, FD-CHR, is vector multiplication Mul. I argued that 
   it is wrong to call the declarations faulty and invalid just because

   there are some invalid calls. I also suggested one way in which
   the declarations can be permitted, while ruling out the faulty call:

   http://www.haskell.org//pipermail/haskell-prime/2006-March/000847.html

   basically, the idea is that FDs specify type-level functions, so
   unless we can demonstrate that those functions are non-strict, we
   need to rule out cyclic type-level programs that feed the range of
   an FD into one of its domain parameters, by a generalized occurs
   check.

   simply looking at the intersection of variables is easy to implement;
   that method is still too conservative (eg, if the range is simly a
   copy of the domain), but adding it to our repertoire of termination 
   checks definitely improves the situation, and is sufficient to permit

   the declarations in example 6, while ruling out the offending call.

5 example 16, CHR, defines an instance that hides an increasing
   type behind an FD. my intuition on that one tells me that we are
   again ignoring the functional character of FDs (as we did in 4). 
   
   instead of ruling out types determined entirely by FDs via the 
   bound variable restriction, as the paper suggests, we could 
   extend the termination check to collect information about 
   FDs. just think of type constructors as simple FDs and try 
   to treat real FDs similarly: 

   adding a constructor around a type variable in the context 
   means we cannot guarantee termination by reasoning about 
   shrinking types. determining a type variable in the context by

   putting it in the range of an FD means we cannot guarantee
   termination by reasoning about shrinking types, unless we
   have some conservative approximation of the relation 
   between domain and range of the FD to tell us so.


   the example case:

   class F a b | a- b
   instance F [a] [[a]]

   clearly shows the range to be more complex than the domain,
   so we can account for that increase in complexity when we 
   see F t x in an instance context.


   if instead, we only had:

   class F a b | a-b
   instance F [[a]] [a]

   the range would be less complex than the domain, so we could
   permit use of this, even though the bound variable condition
   would treat it the same way - forbid it.

there are whole yearly workshops dedicated to termination.
we shouldn't assume that we can reach any satisfactory solution
by a mere handful of restrictions. which means that we need to
add to our repertoire of termination checks, and to keep open 
the option of switching of those checks.


cheers,
claus

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

Re: the MPTC Dilemma (please solve)

[Manuel M T Chakravarty]

Claus Reinke:
  In fact, it's quite worrying that FDs have been around for so long and
  still resisted a thorough understanding.
 
 they don't resist. but as long as progress is example-driven and scary
 stories about FDs supposedly being tricky and inherently non-under-
 standable are more popular than investigations of the issues, there 
 won't be much progress. please don't contribute to that hype.

When I say hard to understand, I mean difficult to formalise.  Maybe I
have missed something, but AFAIK the recent Sulzmann et al. paper is the
first to thoroughly investigate this.  And even this paper doesn't
really capture the interaction with all features of H98.  For example,
AFAIK the CHR formalisation doesn't consider higher kinds (ie, no
constructor classes).

 it is okay to advertize for your favourite features. in fact, I might 
 agree with you that a functional type-class replacement would be 
 more consistent, and would be a sensible aim for the future. 
 
 but current Haskell has type classes, and current practice does use 
 MPTCs and FDs; and you don't do your own case any favours by 
 trying to argue against others advertizing and investigating their's. 

I don't care whether I do my case a favour.  I am not a politician.
There is only one reason that ATs exist: FDs have serious problems.

Two serious problems have little to do with type theory.  They are more
like software engineering problems:

 I. One is nicely documented in

http://www.osl.iu.edu/publications/prints/2003/comparing_generic_programming03.pdf
II. The other one is that if you use FDs to define type-indexed
types, you cannot make these abstract (ie, the representations
leak into user code).  For details, please see the Lack of
abstraction. subsubsection in Section 5 of
http://www.cse.unsw.edu.au/~chak/papers/#assoc

 you reply to a message that is about a month old.

That's what re-locating around half of the planet does to your email
responsiveness...but the topic is still of interest and I got the
impression that your position is still the same.

 for instance, ATS should just be special syntax for a limited, but 
 possibly sufficient and more tractable form of MPTCs/FDs, and 
 as long as that isn't the case in practice because of limitations in
 current implementations or theory, we don't understand either 
 feature set sufficiently well to make any decisions.

ATs are not about special syntax.  Type checking with ATs doesn't not
use improvement, but rather a rewrite system on type terms interleaved
with unification.  This leads to similar effects, but seems to have
slightly different properties.

Actually, I think, much of our disagreement is due to a different idea
of the purpose of a language standard.  You appear to be happy to
standardise a feature that may be replaced in the next standard.  (At
least, both of the choices you propose in your email include
deprecating a feature in Haskell''.)  I don't see that as an acceptable
solution.  A standard is about something that stays.  That people can
rely on.  IMHO if we consider deprecating a feature in Haskell'' again,
we should not include it in Haskell', but leave it as an optional extra
that some systems may experimentally implement and some may not.

Manuel


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

Re: Re[2]: the MPTC Dilemma (please solve)

[Manuel M T Chakravarty]

Ross Paterson:
 On Sun, Mar 19, 2006 at 11:25:44AM -0500, Manuel M T Chakravarty wrote:
  My statement remains:  Why use a relational notation if you can have a
  functional one?
 
 I agree that functions on static data are more attractive than logic
 programming at the type level.  But with associated type synonyms,
 the type level is not a functional language but a functional-logic one.

Your are right, of course.  

Hand-waving-alert
However, the evaluation model is what is known as residuation
in the FL community, which is essentially functional programming
with logic variables and lenient evaluation (a la Id).  As long
as we only have strongly normalising functions, lenient
evaluation and lazy evaluation coincide.  So, for Haskell
programmers, we are on familiar ground.
/Hand-waving-alert

Manuel


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

Re: the MPTC Dilemma (please solve)

[Aaron Denney]

On 2006-03-20, Manuel M T Chakravarty [EMAIL PROTECTED] wrote:
 IMHO if we consider deprecating a feature in Haskell'' again,
 we should not include it in Haskell', but leave it as an optional extra
 that some systems may experimentally implement and some may not.

Possibly true, but it still needs to be standardized so that it will
work the same on different implementations.

-- 
Aaron Denney
--

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

Re: the MPTC Dilemma (please solve)

[Claus Reinke]

For example, AFAIK the CHR formalisation doesn't consider higher 
kinds (ie, no constructor classes).


you're right about interactions in general. but do you think constructor 
classes specifically would pose any interaction problems with FDs?



I don't care whether I do my case a favour.  I am not a politician.
There is only one reason that ATs exist: FDs have serious problems.


you don't solve problems by creating new features from scratch,
with a different theory/formalization to boot. you try to pinpoint the
perceived problems in the old feature, then either transform it to
avoid those problems, or demonstrate that such transformation is
not possible. otherwise, you have the nasty problem of relating 
your new feature/theory to the old one to demonstrate that you've

really improved matters.


Two serious problems have little to do with type theory.  They are more
like software engineering problems:

I. One is nicely documented in
   
http://www.osl.iu.edu/publications/prints/2003/comparing_generic_programming03.pdf


that paper isn't bad as far as language comparisons go, but it focusses
on a rather restricted problem, so I'm surprised that this was part of the
motivation to launch ATS: to reduce the number of parameters in 
combined concepts, we might as well associate types with each

other, instead of types with instances.

variant A: I never understood why parameters of a class declaration
   are limited to variables. the instance parameters just have
   to match the class parameters, so let's assume we didn't
   have that variables-only restriction.

   class Graph (g e v) where
   src :: e - g e v - v
   tgt :: e - g e v - v

   we associate edge and node types with a graph type by
   making them parameters, and extract them by matching.

variant B: I've often wanted type destructors as well as constructors.
   would there be any problem with that?

   type Edge (g e v) = e
   type Vertex (g e v) = v

   class Graph g where
   src :: Edge g - g - Vertex g
   tgt :: Edge g  - g - Vertex g

variant C: the point the paper makes is not so much about the number
   of class parameters, but that the associations for concepts
   should not need to be repeated for every combined concept.
   and, indeed, they need not be

   class Edge g e | g - e
   instance Edge (g e v) e
   class Vertex g v | g - v
   instance Vertex (g e v) v

   class (Edge g e,Vertex g v) = Graph g where
   src :: e - g - v
   tgt :: e - g - v

   (this assumes scoped type variables; also, current GHC,
contrary to its documentation, does not permit entirely 
FD-determined variables in superclass contexts)


all three seem to offer possible solutions to the problem posed in 
that paper, don't they?



   II. The other one is that if you use FDs to define type-indexed
   types, you cannot make these abstract (ie, the representations
   leak into user code).  For details, please see the Lack of
   abstraction. subsubsection in Section 5 of
   http://www.cse.unsw.edu.au/~chak/papers/#assoc


do they have to? if variant C above would not run into limitations
of current implementations, it would seem to extend to cover ATS:

   class C a where
   type CT a

   instance C t0 where
   type CT t0 = t1

would translate to something like:

   class CT a t | a - t
   instance CT t0 t1

   class CT a t = CT a
   instance CT t0 t1 = C t0

as Martin pointed out when I first suggested this on haskell-cafe,
this might lead to parallel recursions for classes C and their type
associations CT, so perhaps one might only want to use this to
hide the extra parameter from user code (similar to calling auxiliary
functions with an initial value for an accumulator).


you reply to a message that is about a month old.


That's what re-locating around half of the planet does to your email
responsiveness...but the topic is still of interest and I got the
impression that your position is still the same.


definitely. I was just unsure how to react - if you really hadn't seen
the messages of the last month, it would be better to let you catch up
(perhaps via the mailing list archive). if you just took that message as
the natural place to attach your contribution to, there's no need to wait.


ATs are not about special syntax.  Type checking with ATs doesn't not
use improvement, but rather a rewrite system on type terms interleaved
with unification.  This leads to similar effects, but seems to have
slightly different properties.


that's what I'm complaining about. if ATs were identified as a subset of
FDs with better properties and nicer syntax, it would be easy to compare.

Re[2]: the MPTC Dilemma (please solve)

[Bulat Ziganshin]

Hello Lennart,

Sunday, March 19, 2006, 4:05:03 AM, you wrote:

LA I have to agree with Manuel.  I write a lot of Haskell code.
LA People even pay me to do it.  I usually stay with Haskell-98,

when i wrote application code, i also don't used extensions very much,
i even don't used Haskell-98 very much and afair don't defined any type
classes at all

but when i gone to writing libraries, that can be used by everyone,
type classes and requirement in even more extensions is what i need
permanently. in particular, i try to write library so what any
conception (stream, Binary, reference, array) can be used in any monad
and that immediately leads me to using MPTC+FD. moreover, problems with
resolving class overloading and other deficiencies of current
unofficial Hugs/GHC standard are permanently strikes me

so, from my point of view, we should leave MPTC+FD+any well-specified
extensions in resolution of overlapping classes. but these should be
seen only as shortcuts for the new type-calculation functions, like
the old-style data definitions now seen as shortcuts for GADT ones

just some examples how this can look:

i had a class which defines default reference type for monads:

class Ref m r | m-r where
  newRef :: a - m (r a)
  readRef :: r a - m a
  writeRef :: r a - a - m ()

instance Ref IO IORef where ...
instance Ref (ST s) (STRef s) where ...


this class allows to write monad-independent code, for example:

doit = do x - newRef 0
  a - readRef x
  writeRef x (a+1)
  readRef x

can be runned in IO or ST monads, or in any monad derived from IO/ST
(with appropriate instance Ref definitions). As you can see, even such
small example require using FDs.



That's all great but not flexible. That we required is a real
functions on type values. In ideal, types should become first-time
values, compile-type computations should be allowed (what resembles
me Template Haskell), and computed types should be allowed to
used in any place where current Haskell allows type literals.
moreover, runtime-computed types can be used for dynamic/generic
programming, but that is beyond of our current theme.

really, Haskell already has functions on types:

type Id a = a
type Two a = (a,a)

and so on. but these definitions don't have full computational (Turing)
power, can't contain several sentences, can't be split among different
modules/places and so on, so on. on the other side, class definitions
are our most powerful type functions, but has very different syntax and
semantic model compared to plain functions, plus had some additional
duties (declaring a family of functions)



how about adding to type functions the full power of ordinal
functions? first, data/newtype declares new type constructor on its
left part in the same way as it defines new data constructors on its
right part:

data List a = Nil | Cons a (List a)

defines Nil and Cons data constructors and List type constructor.
Together all data constructors defined in program plus primitive types
(Int, Char...) defines a full set of types that can be
constructed/analyzed by type construction functions. so, we should
not only allow to construct new more complex types on the right side of
type function, but also allow to analyze complex types on the left
side of function definition! :

type Element (List a) = a
 Element (Array i e) = e
 Element (UArray i e) | Unboxed e = e

cute? i love it :)  i also used pattern guard here, it's a partial
replacement of Prolog's backtracking mechanism. of course, to match
power of type classes, we should allow to split these definitions
among the whole module and even among the many modules. library
type function should be allowed to be extended in application modules
and application definitions should have a priority over library ones

this will allow to rewrite my Ref class as:

type Ref IO = IORef
 Ref (ST s) = STRef s



Next problem is declaring types (to be exact, kinds) of type
functions. currently, kinds are defined only in terms of arity:

type ReturnInt (m :: * - *) = m Int

but what we really want is to declare that `m` is Monad here:

type ReturnInt (m :: Monad) = m Int

or

type ReturnInt :: Monad - *
type ReturnInt m = m Int

i also propose to show kind arity by using just **, *** instead of
current *-*, *-*-*. the above definition can be extended in
user module by:

type ReturnInt (ST s) = Int

but not with

type ReturnInt Int = IO

because last definition break types for both left and right sides



having all this in mind, we can break class definitions into the
lower-level pieces. say,

class Monad m where
return  :: a - m a
fail:: String - m a
instance Monad IO where
return = returnIO
fail   = failIO

translates into:

type Monad :: ** - (a - m a, String - m a)
type Monad IO = (returnIO, failIO)

i.e. Monad is function that translates '**' types into the tuple
containing several functions. well, translation is not ideal, but at
least it seems promising

Re: the MPTC Dilemma (please solve)

[Jean-Philippe Bernardy]

On 3/18/06, Manuel M T Chakravarty [EMAIL PROTECTED] wrote:
 Here addition and multiplication on Peano numerals using MPTCs and FDs:

 data Z
 data S a

 class Add a b c | a b - c
 instance Add Z b b
 instance Add a b c = Add (S a) b (S c)

 class Mul a b c | a b - c
 instance Mul Z b Z
 instance (Mul a b c, Add c b d) = Mul (S a) b d

 It's a mess, isn't it.  Besides, this is really untyped programming.
 You can add instances with arguments of types other than Z and S without
 the compiler complaining.  So, we are not simply using type classes for
 logic programming, we use them for untyped logic programming.  Not very
 Haskell-ish if you ask me.

 I'd rather write the following:

   kind Nat = Z | S Nat

   type Add Z (b :: Nat) = b
Add (S a) (b :: Nat) = S (Add a b)

   type Mul Z (b :: Nat) = Z
Mul (S a) (b :: Nat) = Add (Mul a b) b

 Well, actually, I'd like infix type constructors and some other
 syntactic improvements, but you get the idea.  It's functional and
 typesafe.  Much nicer.

Indeed, this looks all very good and I truly believe this is the
direction we should move in.

Still, a question: do you propose to go as far as to replace the
traditional single parameter type-classes with /partial/ type
constructors? This is really a naive question -- I don't claim to
understand everything this implies.

A couple examples to illustrate my thinking:


type Show :: +  -- where + is representing an (open) subset of the * kind.
type Show = s  -- 's' binds to the result of the partial type function
being defined
  where show :: s - String

-- alternative, maybe showing better the closing gap between classes and types
-- type Show :: +
--   where show :: Show - String

type Show = Char
   where show = ...

type Show = [s]
   where s = Show   -- constraining the type variable s
 show = ...

-- alternatively
-- type Show = [Show]
--   where show = ...


-
-- Revisiting a familiar example

type Collect :: + - +
type Collect a = c
   where insert :: a - c - c

type Collect elem = Set elem
   where elem = Ord
 insert = ...



-- Here begins the fun.

type Functor :: * - +
type Functor = f
  where map :: (a - b) - f a - f b


Cheers,
JP.
___
Haskell-prime mailing list
Haskell-prime@haskell.org
http://haskell.org/mailman/listinfo/haskell-prime

Re: Re[2]: the MPTC Dilemma (please solve)

[Manuel M T Chakravarty]

Bulat Ziganshin:
 Hello Lennart,
 
 Sunday, March 19, 2006, 4:05:03 AM, you wrote:
 
 LA I have to agree with Manuel.  I write a lot of Haskell code.
 LA People even pay me to do it.  I usually stay with Haskell-98,
 
 when i wrote application code, i also don't used extensions very much,
 i even don't used Haskell-98 very much and afair don't defined any type
 classes at all
 
 but when i gone to writing libraries, that can be used by everyone,
 type classes and requirement in even more extensions is what i need
 permanently. in particular, i try to write library so what any
 conception (stream, Binary, reference, array) can be used in any monad
 and that immediately leads me to using MPTC+FD. moreover, problems with
 resolving class overloading and other deficiencies of current
 unofficial Hugs/GHC standard are permanently strikes me

Libraries are a means, not an end.  The fact still remains.  Most
programs don't need MPTCs in an essential way.  It's convenient to have
them, but they are not essential.

 i had a class which defines default reference type for monads:
 
 class Ref m r | m-r where
   newRef :: a - m (r a)
   readRef :: r a - m a
   writeRef :: r a - a - m ()
 
 instance Ref IO IORef where ...
 instance Ref (ST s) (STRef s) where ...
 
 
 this class allows to write monad-independent code, for example:
 
 doit = do x - newRef 0
   a - readRef x
   writeRef x (a+1)
   readRef x
 
 can be runned in IO or ST monads, or in any monad derived from IO/ST
 (with appropriate instance Ref definitions). As you can see, even such
 small example require using FDs.
[..]

 this will allow to rewrite my Ref class as:
 
 type Ref IO = IORef
  Ref (ST s) = STRef s

You are going in the right direction, but what you want here are
associated types; i.e., you want type functions that are open and can be
extended (in the same way as classes can be extended by adding new
instances).  Your example reads as follows with associated types:

  class Monad m = RefMonad m where
type Ref m :: * - *
newRef :: a - m (Ref m a)
readRef :: Ref m a - m a
writeRef :: Ref m a - a - m ()

  instance RefMonad IO where 
type Ref IO = IORef
...
  instance RefMonad (ST s) where
type Ref (ST s) = STRef s
...

My statement remains:  Why use a relational notation if you can have a
functional one?  (The RefMonad class is btw very similar to a functor of
ML's module system.[*])  See 

  http://hackage.haskell.org/trac/haskell-prime/wiki/AssociatedTypes

for more details on associated types.

Manuel

[*] Cf http://www.informatik.uni-freiburg.de/~wehr/diplom/

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

Re[4]: the MPTC Dilemma (please solve)

[Bulat Ziganshin]

Hello Manuel,

Sunday, March 19, 2006, 7:25:44 PM, you wrote:

 i had a class which defines default reference type for monads:
 
 class Ref m r | m-r where

to be exact,

class Ref m r | m-r, r-m where
   newRef :: a - m (r a)
   readRef :: r a - m a
   writeRef :: r a - a - m ()

or even worser:

class Ref2 m r a | m a-r, r-m
instance (Unboxed a) = Ref2 IO IOURef a
instance (!Unboxed a) = Ref2 IO IORef a
instance (Unboxed a) = Ref2 (ST s) (STURef s) a
instance (!Unboxed a) = Ref2 (ST s) (STRef s) a

MMTC My statement remains:  Why use a relational notation if you can have a
MMTC functional one?

how about these examples?

MMTC   class Monad m = RefMonad m where
MMTC type Ref m :: * - *

can i use `Ref` as type function? for example:

data StrBuffer m = StrBuffer (Ref m Int)
 (Ref m String)
 
-- 
Best regards,
 Bulatmailto:[EMAIL PROTECTED]

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

Re: Re[2]: the MPTC Dilemma (please solve)

[Ross Paterson]

On Sun, Mar 19, 2006 at 11:25:44AM -0500, Manuel M T Chakravarty wrote:
 My statement remains:  Why use a relational notation if you can have a
 functional one?

I agree that functions on static data are more attractive than logic
programming at the type level.  But with associated type synonyms,
the type level is not a functional language but a functional-logic one.

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

Re: Re[2]: the MPTC Dilemma (please solve)

[Martin Sulzmann]

Manuel M T Chakravarty writes:
  The big question is: do we really want to do logic programming over
  types?  I'd say, no!

With ATs you're still doing logic programming if you like or not.

As Ross Paterson writes:
  I agree that functions on static data are more attractive than logic
  programming at the type level.  But with associated type synonyms,
  the type level is not a functional language but a functional-logic one.

The point is here really that you may think you define
a type function, e.g.

type F [a] = [F a]

though, these type definitions behave more like relations,
cause (type) equations behave bi-directionally.


Manuel M T Chakravarty writes:
  My statement remains:  Why use a relational notation if you can have a
  functional one?

Because a relational notation is strictly stronger. 

Some time ago I asked the following:

Write the AT equivalent of the following FD program.

zip2 :: [a]-[b]-[(a,b)]
zip2 = ... -- standard zip
class Zip a b c | c-a, c-b where
 zip :: [a]-[b]-c
instance Zip a b [(a,b)] where-- (Z1)
 zip = zip2
instance Zip (a,b) c e = Zip a b ([c]-e) where  -- (Z2)
 zip as bs cs = zip (zip2 as bs) cs

Specifying the FD improvement conditions via AT type functions
is a highly non-trivial task.
Check out Section 2 in
[October 2005]  Associated Functional Dependencies 
http://www.comp.nus.edu.sg/~sulzmann/
for the answer.

Sure, ATs provide a nice syntax for a specific kind of type class
programs.  Though, as I've pointed out before any AT program can be
encoded with FDs but the other direction does not hold necessarily.
See the above paper for details.


Manuel M T Chakravarty writes:
   
   From: Martin Sulzmann [EMAIL PROTECTED]
   Subject: MPTC/FD dilemma 
   
   - ATs (associated types) will pose the same challenges.
 That is, type inference relies on dynamic termination checks.
  
  Can you give an example?


There's nothing wrong with ATs as described in the ICFP'05 paper.
The problem is that some simple extension easily lead to undecidable
type inference.

Recall the following discussion:
http://www.haskell.org//pipermail/haskell-cafe/2006-February/014609.html

The point here is really that type inference for ATs and FDs is
an equally hard problem:
http://www.haskell.org//pipermail/haskell-cafe/2006-February/014680.html


Another thing, here's an excerpt of the current summary of the MPTC
dilemma from
http://haskell.galois.com/cgi-bin/haskell-prime/trac.cgi/wiki


Multi Parameter Type Classes Dilemma ¦

Options for solving the dilemma ¦   
2. Put AssociatedTypes on the fast-track for sainthood

Associated Types ¦

   Cons ¦   
* Only a prototype implementation so far 

This is a *inaccurate* and highly *misleading* summary.

Without some formal argument you cannot simply say that ATs are
better than FDs. In some situations, ATs may have a better syntax
than FDs. Though, this is a matter of taste. More seriously, ATs
require the programmer to write *all* improvement rules
explicitly. This can be a fairly challenging task. See the above zip
example.

I understand that you want to push ATs. It's a good thing to seek
for alternatives. But typing and translating ATs is as challenging
as typing and translating FDs (I've left out the translation issue,
cause this leads to far here).

Martin

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

Re: the MPTC Dilemma (please solve)

[Manuel M T Chakravarty]

Claus Reinke:
 however, the underlying problem is not limited to MPTCs, and FDs 
 are not the only attempt to tackle the problem. so I agree with Isaac: 
 getting a handle on this issue is imperative for Haskell', because it will 
 be the only way forward when trying to standardize at least those of 
 the many extensions that have been around longer than the previous 
 standard Haskell 98. and if Haskell' fails to do this, it fails.

Please keep things in perspective:

(A) It's not as if every interesting program (or even the majority of
interesting programs) use(s) MPTCs.

(B) I don't think the time for which an extension has been around is
particularly relevant.  One of the big selling points of Haskell is that
it's quite well defined, and hence, its semantics is fairly well
understood and sane - sure, there are dark corners, but compared to
other languages of the same size, we are in good shape.  If we include
half-baked features, we weaken the standard.

In fact, it's quite worrying that FDs have been around for so long and
still resisted a thorough understanding.

Manuel


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

Re: the MPTC Dilemma (please solve)

[Manuel M T Chakravarty]

Isaac Jones:
 I'm forwarding an email that Martin Sulzmann asked me to post on his
 behalf.
 
 
 From: Martin Sulzmann [EMAIL PROTECTED]
 Subject: MPTC/FD dilemma 
 
 - ATs (associated types) will pose the same challenges.
   That is, type inference relies on dynamic termination checks.

Can you give an example?

Manuel


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

Re: the MPTC Dilemma (please solve)

[Lennart Augustsson]

I have to agree with Manuel.  I write a lot of Haskell code.
People even pay me to do it.  I usually stay with Haskell-98,
and I don't think it's a great hardship.  Sure, there's fancy
stuff I can't do then, but I'd much rather have a well understood
somewhat less powerful language.

I think the right way forward is more along the lines of
associated type and type level functions rather than
MPTC and FDs.

-- Lennart

Manuel M T Chakravarty wrote:

Claus Reinke:
however, the underlying problem is not limited to MPTCs, and FDs 
are not the only attempt to tackle the problem. so I agree with Isaac: 
getting a handle on this issue is imperative for Haskell', because it will 
be the only way forward when trying to standardize at least those of 
the many extensions that have been around longer than the previous 
standard Haskell 98. and if Haskell' fails to do this, it fails.


Please keep things in perspective:

(A) It's not as if every interesting program (or even the majority of
interesting programs) use(s) MPTCs.

(B) I don't think the time for which an extension has been around is
particularly relevant.  One of the big selling points of Haskell is that
it's quite well defined, and hence, its semantics is fairly well
understood and sane - sure, there are dark corners, but compared to
other languages of the same size, we are in good shape.  If we include
half-baked features, we weaken the standard.

In fact, it's quite worrying that FDs have been around for so long and
still resisted a thorough understanding.

Manuel


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



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

Re: relaxed instance rules spec (was: the MPTC Dilemma (please solve))

[Ben Rudiak-Gould]

John Meacham wrote:

On Thu, Mar 02, 2006 at 03:53:45AM -, Claus Reinke wrote:

the problem is that we have somehow conjured up an infinite
type for Mul to recurse on without end! Normally, such infinite
types are ruled out by occurs-checks (unless you are working
with Prolog III;-), so someone forgot to do that here. why?
where? how?


Polymorphic recursion allows the construction of infinite types if I
understand what you mean.


No, that's different. An infinite type can't be written in (legal) Haskell. 
It's something like


type T = [T]

-- Ben

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

RE: relaxed instance rules spec (was: the MPTC Dilemma (please solve))

[Simon Peyton-Jones]

Claus,

I urge you to read our paper Understanding functional dependencies via
Constraint Handling Rules, which you can find here
http://research.microsoft.com/%7Esimonpj/papers/fd%2Dchr/.

It will tell you more than you want to know about why relaxing
apparently-conservative rules is entirely non-trivial.   It's one of
those areas in which it is easy to suggest a plausible-sounding
alternative, but much harder to either prove or disprove whether the
alternative a sound one.

The paper describes rules we are reasonably sure of.   It would be great
to relax those rules.  But you do need to have a proof that the
relaxation preserves the properties we want.  Go right ahead!  The paper
provides a good framework for such work, I think.

Simon

| -Original Message-
| From: Claus Reinke [mailto:[EMAIL PROTECTED]
| Sent: 28 February 2006 19:54
| To: Simon Peyton-Jones; haskell-prime@haskell.org
| Subject: relaxed instance rules spec (was: the MPTC Dilemma (please
solve))
| 
| The specification is here:
|
http://www.haskell.org/ghc/dist/current/docs/users_guide/type-extension
s.html#instance-decls
| 
| two questions/suggestions about this:
| 
| 1. there are other termination criteria one migh think of, though
| many will be out because they are not easy to specify. but here
| is an annoyingly simple example that doesn't fit the current rules
| even though it is clearly terminating (it's not even recursive):
| 
| class Fail all -- no instances!
| 
| class TypeNotEq a b
| instance Fail a = TypeNotEq a a
| instance TypeNotEq a b
| 
| class Test a b where test :: a - b - Bool
| instance TypeNotEq a b = Test a b where test _ _ = False
| instance Test a a where test _ _ = True
| 
| main = print $ (test True 'c', test True False)
| 
| never mind the overlap, the point here is that we redirect from
| Test a b to TypeNotEq a b, and ghc informs us that the
| Constraint is no smaller than the instance head.
| 
| it is true that the parameters don't get smaller (same number,
| same number of constructors, etc.), but they are passed to a
| smaller predicate (in terms of call-graph reachability: there
| are fewer predicates reachable from TypeNotEq than from
| Test - in particular, Test is not reachable from TypeNotEq).
| 
| this is a non-local criterion, but a fairly simple one. and it
seems
| very strange to invoke undecidable instances for this example
| (or is there anything undecidable about it?).
| 
| 2. the coverage condition only refers to the instance head. this
| excludes programs such as good old record selection (which
| should terminate because it recurses over finite types, and is
| confluent -in fact deterministic- because of best-fit overlap
| resolution):
| 
| -- | field selection
| infixl #?
| 
| class Select label val rec | label rec - val where
|   (#?) :: rec - label - val
| 
| instance Select label val ((label,val),r) where
|   ((_,val),_) #? label = val
| 
| instance Select label val r = Select label val (l,r) where
|   (_,r)   #? label = r #? label
| 
| now, it is true that in the second instance declaration, val is
| not covered in {label,(l,r)}. however, it is covered in the
recursive
| call, subject to the very same FD, if that recursive call complies
| with the (recursive) coverage criterion. in fact, for this
particular
| task, that is the only place where it could be covered.
| 
| would it be terribly difficult to take such indirect coverage (via
| the instance constraints) into account? there'd be no search
| involved (the usual argument against looking at the constraints),
| and it seems strange to exclude such straightforward consume
| a type recursions, doesn't it?
| 
| cheers,
| claus

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

Re: the MPTC Dilemma (please solve)

[John Meacham]

On Tue, Feb 28, 2006 at 07:12:28PM -, Claus Reinke wrote:
 Anyway, there is already a ticket for overlapping instances, I think --
 why don't you just add to that.
 
 that might work. apart from the fact that I really, really hate the 
 braindead wiki markup processor, especially when editing through
 that tiny ticket change field instead of loading up text. I went through
 that experience once, when Isaac suggested the same for my labels
 proposal - I don't want to have to do that again.
 

MozEX is your friend:
  http://mozex.mozdev.org/

it lets you click on any text field on the web and say 'edit in vim' (or
whatever editor you choose)

John

-- 
John Meacham - ⑆repetae.net⑆john⑈
___
Haskell-prime mailing list
Haskell-prime@haskell.org
http://haskell.org/mailman/listinfo/haskell-prime

Re: relaxed instance rules spec (was: the MPTC Dilemma (please solve))

[John Meacham]

On Thu, Mar 02, 2006 at 03:53:45AM -, Claus Reinke wrote:
 - Mul recurses down a type in its second parameter
 - types in Haskell are finite
 - there is a non-terminating Mul inference
 
 the problem is that we have somehow conjured up an infinite
 type for Mul to recurse on without end! Normally, such infinite
 types are ruled out by occurs-checks (unless you are working
 with Prolog III;-), so someone forgot to do that here. why?
 where? how?

Polymorphic recursion allows the construction of infinite types if I
understand what you mean. if you are clever (or unlucky) you can get
jhcs middle end to go into an infinite loop by using them.

 -- an infinite binary tree
 data Bin a = Bin a (Bin (a,a))


John
-- 
John Meacham - ⑆repetae.net⑆john⑈
___
Haskell-prime mailing list
Haskell-prime@haskell.org
http://haskell.org/mailman/listinfo/haskell-prime

Re: the MPTC Dilemma (please solve)

[Claus Reinke]

You addressed this to me -- but I'm an advocate for rather conservative
extensions whereas you are calling for extensions that go beyond what
any current implementation can do.


generally, that may be true,-) but in this specific case, I was just asking 
for an effort to document the differences in current handling of extended
Haskell in hugs and ghc, by collecting test cases such as those I included. 

whether or not the haskell' process manages to help eradicate those 
differences is another matter, but collecting them seems a useful basis 
for decisions, hence a task rather than a proposal. I addressed that to 
you because (a) I was hoping this more moderate approach would be 
down your alley and (b) because you have a stake in this at ghc hq, 
and probably would want to collect the test cases for possible fixing.


I guess I will create the ticket myself, but if no committee member
or implementer has a stake in it, that won't do much good..


Anyway, there is already a ticket for overlapping instances, I think --
why don't you just add to that.


that might work. apart from the fact that I really, really hate the 
braindead wiki markup processor, especially when editing through

that tiny ticket change field instead of loading up text. I went through
that experience once, when Isaac suggested the same for my labels
proposal - I don't want to have to do that again.


If you send me Wiki-marked-up text I'll gladly paste it in for you.


perhaps I'll just restrict myself to attaching my example code to
some ticket (are guests allowed to update attachments?). will see..

thanks,
claus

| -Original Message-
| From: Claus Reinke [mailto:[EMAIL PROTECTED]
| Sent: 25 February 2006 15:33
| To: Simon Peyton-Jones
| Cc: haskell-prime@haskell.org
| Subject: Re: the MPTC Dilemma (please solve)
| 
| | Is the behaviour of GHC with -fallow-undecidable-instances (and

| | -fcontext-stack) well-understood and specifiable?
| I would not say that it's well-specified, no.
| 
| to start improving that situation, could we please have a task ticket

| for document differences in unconstrained instance handling, then
| ask everyone to attach source examples showing such differences?
| [can guests attach code to task tickets?]
| 
| the hope being, of course, that implementations nominally providing

| the same feature will eventually converge on providing the same
| interpretation of all programs using that feature.
| 
| an example of the current oddities (at least they seem odd to me;):

| both hugs and ghc claim to resolve overlapping instances in favour
| of the most specific instance declaration. both claim that functional
| dependencies uniquely determine the range types from the domain
| types. but they do not agree on which programs to accept when
| we try to combine best-match with FDs.
| 
| I've already given an example where ghc allows me to define

| record selection, while hugs complains that the overlap violates
| the FDs.
| 
| I reported that as a hugs bug, because I think the best-match

| resolution of overlaps should ensure that the FD violation cannot
| happen, so the code should be valid. there are different ways to
| interpret FDs (something to check, or something to use), but it
| seemed that ghc was doing the right thing there. thread start:
| 
| http://www.haskell.org//pipermail/hugs-bugs/2006-February/001560.html
| 
| but after further experimentation, I'm not longer sure that ghc

| is doing the right thing for the right reasons. here is a tiny example
| of one of the disagreements:
| 
| {- ghc ok

|hugs Instance is more general than a dependency allows -}
| 
| class C a b | a - b

| instance C a b
| 
| so what is ghc doing there? is it going to guarantee that b will

| always be uniquely determined?
| 
| {- ghc ok

|hugs Instance is more general than a dependency allows -}
| 
| class C b | - b where c :: b

| instance C b where c = error b
| 
| safely m = m `CE.catch` print

| main = do
|   safely $ print $ (c::Int)
|   safely $ print $ (c::Bool)
|   safely $ print [id,c]
| 
| oh, apparently not. unless b is uniquely determined to be universally

| quantified, and the instantiations happen after instance selection.
| 
| {- ghc ok

|hugs Instance is more general than a dependency allows -}
| 
| class C b | - b where c :: b

| instance C b where c = error b
| 
| class D a where d :: a - String

| instance C a = D a where d a = a
| instance C Int = D Int where d a = Int
| 
| -- try at ghci prompt:  (d 1,d (1::Int))

| -- gives: (a,Int)
| 
| so that parameter of C isn't all that unique. at least not long enough

| to influence instance selection in D.
| 
| comments?
| 
| cheers,

| claus

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

Re: the MPTC Dilemma (please solve)

[Claus Reinke]

continuing the list of odd cases in type class handling, here is a
small example where overlap resolution is not taken into account
when looking at FDs. 

context: both hugs and ghc resolve instance overlaps in favour 
of the most specific declaration.


so the following works in both ghc (darcs, 25022006) and 
hugs (minhugs 20051031):


   {- both ghc and hugs accept without 3rd par and FD
  neither accepts with 3rd par and FD -}

   data T = T deriving Show
   data F = F deriving Show

   classTEQ a b {- tBool | a b - tBool -} where teq :: a - b - Bool
   instance TEQ a a {- T-} where teq _ _ = True
   instance TEQ a b {- F-} where teq _ _ = False

   test = print (teq True 'c', teq True False)

and both print (False,True), so best-fit overlap resolution entirely 
determines which instance to choose! 

now, if we uncomment the third class parameter, they both complain 
(as expected, though about different things).


however, if we also uncomment the functional dependency, to fix 
the ambiguity wrt the 3rd parameter, both complain that this FD 
is in conflict/inconsistent with the instances!


as far as i understand it, the potential inconsistency should have 
been eliminated by the best-fit overlap resolution, so I submit this

is a bug (and unlike the earlier example I submitted to hugs-bugs,
this fails with both hugs and ghc; and it is less open to alternative
interpretations, I hope).

cheers,
claus

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

RE: the MPTC Dilemma (please solve)

[Simon Peyton-Jones]

I would not say that it's well-specified, no.   What we do know is this:
GHC may loop if you use -fallow-undecidable-instances -- but if it
terminates, the program is well typed and should not go wrong at
runtime.

S

| -Original Message-
| From: [EMAIL PROTECTED]
[mailto:[EMAIL PROTECTED] On Behalf Of
| Ashley Yakeley
| Sent: 21 February 2006 20:13
| To: haskell-prime@haskell.org
| Subject: Re: the MPTC Dilemma (please solve)
| 
| Simon Peyton-Jones wrote:
| 
|  Of course -fallow-undecidable-instances still lifts all
restrictions,
|  and then all bets are off.
| 
| Is the behaviour of GHC with -fallow-undecidable-instances (and
| -fcontext-stack) well-understood and specifiable? It is a very useful
| option, as you can join (meet?) classes like this:
| 
|class P a
|class Q a
| 
|class (P a,Q a) = PQ a
|instance (P a,Q a) = PQ a
| 
| --
| Ashley Yakeley
| 
| ___
| Haskell-prime mailing list
| Haskell-prime@haskell.org
| http://haskell.org/mailman/listinfo/haskell-prime
___
Haskell-prime mailing list
Haskell-prime@haskell.org
http://haskell.org/mailman/listinfo/haskell-prime

Re: the MPTC Dilemma (please solve)

[Martin Sulzmann]

When I said type class acrobats I didn't mean to make fun
of people like you who use type classes in a very skillfull way.
Though, I tried (successfully :) ) to be provocactive.

I agree with you there's a real need for unrestricted type class
programming. After all, the Hindley/Milner subset of Haskell already
allows us to write non-terminating, buggy programs. So, what's
the differences if we allow for the same on the level of types!?

The trouble I have with the current practice of type class programming
is that it's not very principled (yes, I'm provocactive again).
People learn how to write type class programs by observing the
behavior of a specific implementation and sometimes the results
are quite unexpected.

I have been mentioning CHRs before as a very useful tool to study
FDs. In fact, CHRs go way beyond FDs see A Theory of Overloading.
I claim that when it comes to unrestricted type class programming
CHRs are the way to go. CHRs have a clean semantic meaning and
precisely explain the meaning of type class programs.

Martin



Claus Reinke writes:
   I'm forwarding an email that Martin Sulzmann asked me to post on his
   behalf.
  
  thanks. well, that is one view of things. but it is certainly not the only 
  one.
  
  first, about those acrobatics: my type-class-level programs tend to
  start out as straightforward logic programs over types - no acrobatics 
  involved, easy to understand. the acrobatics start when I'm trying to 
  fit those straightforward programs into the straightjackets imposed 
  by current systems - be they explicit restrictions or accidental 
  limitations. wrestling them leads to the need to introduce complex 
  work-arounds and implementation-specific tricks into the formerly
  clean logic programs.
  
  the restrictions tend to be artificial and full of odd corners, rather 
  than smooth or natural, and the limitations tend to be the result of 
  not thinking the problem through. so one could say that neither of
  the levels proposed by Martin is ready for standardization. or, one
  could be pragmatic and standardize both levels, well knowing that
  neither is going to be the final word.
  
  second, about the proposal to ignore overlapping instances for the
  moment: that moment has long passed - iirc, undecidable and 
  overlapping instances have been around for longer than the current
  standard Haskell 98. they provide recursion and conditionals (via
  best-match pattern-matching) for logic programming over types.
  they are overdue for inclusion in the standard, and it is time to stop 
  closing our eyes to this fact.
  
  third, understanding FDs via CHRs is very nice, and a good start
  that I hope to see expanded on rather sooner than later. but (a) 
  there is a big discrepancy between the language studied there and 
  current practice, so this work will have to catch on before it can
  be applied; and (b) the main issue with unconstrained type-class-
  level programming is not that it tackles a semi-decidable problem.
  
  in fact, the usual Prolog system only provides an _incomplete_ 
  implementation of almost the same semi-decidable problem. but it 
  provides a well-defined and predictable implementation, so
  programmers can live with that (with a few well-known exceptions).
  
  the two problems are not quite the same, because we extract
  programs from type-class-level proofs. so not only do we need
  the result to be uniquely determined (coherence), we also need
  the proof to be un-ambiguous (or we might get different programs
  depending on the proof variant chosen).
  
  but, and this is an important but: trying to restrict the permissable
  programs so that neither incoherence nor ambiguity can arise in 
  the first place is only _one_ way to tackle the issue; the other
  direction that needs to be explored is to give programmers control
  enough to disambiguate and to restore coherence where needed.
  
  so, I am quite happy with splitting the bigger problem into two
  levels: restrictive programs corresponding to the current state of
  art in formal studies of the problem, and unconstrained programs
  catering for the current state of art in programming practice. just
  as long as both levels are included in the standard, and both levels
  receive the further attention they need.
  
  as far as I understand, this should not pose a problem for 
  implementors, as they usually implement the simpler unconstrained 
  variant first, then add restrictions to conform to the standard.
  
  cheers,
  claus
  
   - There's a class of MPTC/FD programs which enjoy sound, complete
and decidable type inference. See Result 1 below. I believe that
hugs and ghc faithfully implement this class.
Unfortunately, for advanced type class acrobats this class of
programs is too restrictive.
   
   - There's a more expressive class of MPTC/FD programs which enjoy
sound and complete type inference if we can guarantee termination
by for example 

RE: the MPTC Dilemma (please solve)

[Simon Peyton-Jones]

With help from Martin Sulzmann and Ross Paterson, GHC (HEAD) now
implements a richer form of functional dependencies than Mark Jones's
version, but still decidable etc.  The rules for what must appear in the
context of an instance declaration are also relaxed.  

The specification is here:

http://www.haskell.org/ghc/dist/current/docs/users_guide/type-extensions
.html#instance-decls

I think this is a step forward, and a serious candidate for Haskell'.  I
think that if you stick to these rules, everything is nailed down as
Martin so rightly says it should be.  And I am not sure we can go much
further.

Of course -fallow-undecidable-instances still lifts all restrictions,
and then all bets are off.

Many thanks to Ross and Martin.  You can try it out by downloading a GHC
snapshot (or by building from source).

Simon

| -Original Message-
| From: [EMAIL PROTECTED]
[mailto:[EMAIL PROTECTED] On Behalf Of
| isaac jones
| Sent: 11 February 2006 01:29
| To: haskell-prime@haskell.org
| Subject: the MPTC Dilemma (please solve)
| 
| I've created a wiki page and a ticket to record solutions to what I'm
| calling the Multi Parameter Type Class Dilemma.  It's summarized
| thusly:
| 
| MultiParamTypeClasses are very useful, but mostly in the context of
| FunctionalDependencies. They are particularly used in the monad
| transformer library found in fptools. The dilemma is that functional
| dependencies are very, very tricky (spj). AssociatedTypes are
| promising but unproven. Without a solution, Haskell' will be somewhat
| obsolete before it gets off the ground.
| 
| I've proposed a few solutions.  Please help to discover more solutions
| and/or put them on the ticket/wiki.
| 
| Wiki page:
| http://hackage.haskell.org/trac/haskell-prime/ticket/90
| 
| Ticket:
|
http://hackage.haskell.org/trac/haskell-prime/wiki/MultiParamTypeClasses
Dilemma
| 
| 
| peace,
| 
|   isaac
| 
| 
| 
| --
| isaac jones [EMAIL PROTECTED]
| 
| ___
| Haskell-prime mailing list
| Haskell-prime@haskell.org
| http://haskell.org/mailman/listinfo/haskell-prime
___
Haskell-prime mailing list
Haskell-prime@haskell.org
http://haskell.org/mailman/listinfo/haskell-prime

Re: the MPTC Dilemma (please solve)

[Claus Reinke]

I'm forwarding an email that Martin Sulzmann asked me to post on his
behalf.


thanks. well, that is one view of things. but it is certainly not the only one.

first, about those acrobatics: my type-class-level programs tend to
start out as straightforward logic programs over types - no acrobatics 
involved, easy to understand. the acrobatics start when I'm trying to 
fit those straightforward programs into the straightjackets imposed 
by current systems - be they explicit restrictions or accidental 
limitations. wrestling them leads to the need to introduce complex 
work-arounds and implementation-specific tricks into the formerly

clean logic programs.

the restrictions tend to be artificial and full of odd corners, rather 
than smooth or natural, and the limitations tend to be the result of 
not thinking the problem through. so one could say that neither of

the levels proposed by Martin is ready for standardization. or, one
could be pragmatic and standardize both levels, well knowing that
neither is going to be the final word.

second, about the proposal to ignore overlapping instances for the
moment: that moment has long passed - iirc, undecidable and 
overlapping instances have been around for longer than the current

standard Haskell 98. they provide recursion and conditionals (via
best-match pattern-matching) for logic programming over types.
they are overdue for inclusion in the standard, and it is time to stop 
closing our eyes to this fact.


third, understanding FDs via CHRs is very nice, and a good start
that I hope to see expanded on rather sooner than later. but (a) 
there is a big discrepancy between the language studied there and 
current practice, so this work will have to catch on before it can

be applied; and (b) the main issue with unconstrained type-class-
level programming is not that it tackles a semi-decidable problem.

in fact, the usual Prolog system only provides an _incomplete_ 
implementation of almost the same semi-decidable problem. but it 
provides a well-defined and predictable implementation, so

programmers can live with that (with a few well-known exceptions).

the two problems are not quite the same, because we extract
programs from type-class-level proofs. so not only do we need
the result to be uniquely determined (coherence), we also need
the proof to be un-ambiguous (or we might get different programs
depending on the proof variant chosen).

but, and this is an important but: trying to restrict the permissable
programs so that neither incoherence nor ambiguity can arise in 
the first place is only _one_ way to tackle the issue; the other

direction that needs to be explored is to give programmers control
enough to disambiguate and to restore coherence where needed.

so, I am quite happy with splitting the bigger problem into two
levels: restrictive programs corresponding to the current state of
art in formal studies of the problem, and unconstrained programs
catering for the current state of art in programming practice. just
as long as both levels are included in the standard, and both levels
receive the further attention they need.

as far as I understand, this should not pose a problem for 
implementors, as they usually implement the simpler unconstrained 
variant first, then add restrictions to conform to the standard.


cheers,
claus


- There's a class of MPTC/FD programs which enjoy sound, complete
 and decidable type inference. See Result 1 below. I believe that
 hugs and ghc faithfully implement this class.
 Unfortunately, for advanced type class acrobats this class of
 programs is too restrictive.

- There's a more expressive class of MPTC/FD programs which enjoy
 sound and complete type inference if we can guarantee termination
 by for example imposing a dynamic check.  See Result 2 below. Again,
 I believe that  hugs and ghc faithfully implement this class if they
 additionally implement a dynamic termination check.
 Most type class acrobats should be happy with this class I believe.

Let's take a look at the combination of FDs and well-behaved instances.
By well-behaved instances I mean instances which are non-overlapping and
terminating. From now on I will assume that instances must be well-behaved.
The (maybe) surprising observation is that the combination
of FDs and well-behaved instances easily breaks completeness and
decidability of type inference. Well, all this is well-studied.
Check out
[February 2006] Understanding Functional Dependencies via Constraint
Handling Rules by Martin Sulzmann, Gregory J. Duck, Simon Peyton-Jones
and Peter J. Stuckey
which is available via my home-page.

Here's a short summary of the results in the paper:

Result 1:
To obtain sound (we always have that), complete and decidable type inference
we need to impose
   - the Basic Conditions (see Sect4)
 (we can replace the Basic Conditions by any conditions which guarantees
  that instances are well-behaved. I'm ignoring here
  super classes for simplicity)
  

Re: the MPTC Dilemma (please solve)

[Ross Paterson]

On Sat, Feb 18, 2006 at 12:26:36AM +, Ross Paterson wrote:
 Martin Sulzmann [EMAIL PROTECTED] writes:
  Result2:
  Assuming we can guarantee termination, then type inference
  is complete if we can satisfy
 - the Bound Variable Condition,
 - the Weak Coverage Condition, 
 - the Consistency Condition, and
 - and FDs are full.
  Effectively, the above says that type inference is sound,
  complete but semi-decidable. That is, we're complete
  if each each inference goal terminates.
 
 I think that this is a little stronger than Theorem 2 from the paper,
 which assumes that the CHR derived from the instances is terminating.
 If termination is obtained via a depth limit (as in hugs -98 and ghc
 -fallow-undecidable-instances), it is conceivable that for a particular
 goal, one strategy might run into the limit and fail, while a different
 strategy might reach success in fewer steps.

Rereading, I see you mentioned dynamic termination checks, but not
depth limits.  Can you say a bit more about termination?  It seems to
be crucial for your proofs of confluence.

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

Re: the MPTC Dilemma (please solve)

[Ross Paterson]

Martin Sulzmann [EMAIL PROTECTED] writes:
 - There's a class of MPTC/FD programs which enjoy sound, complete
   and decidable type inference. See Result 1 below. I believe that
   hugs and ghc faithfully implement this class.
   Unfortunately, for advanced type class acrobats this class of
   programs is too restrictive.

Not just them: monad transformers also fall foul of these restrictions.
The restrictions can be relaxed to accomodate them (as you do with the
Zip class), but the rules become more complicated.

 Result2:
 Assuming we can guarantee termination, then type inference
 is complete if we can satisfy
- the Bound Variable Condition,
- the Weak Coverage Condition, 
- the Consistency Condition, and
- and FDs are full.
 Effectively, the above says that type inference is sound,
 complete but semi-decidable. That is, we're complete
 if each each inference goal terminates.

I think that this is a little stronger than Theorem 2 from the paper,
which assumes that the CHR derived from the instances is terminating.
If termination is obtained via a depth limit (as in hugs -98 and ghc
-fallow-undecidable-instances), it is conceivable that for a particular
goal, one strategy might run into the limit and fail, while a different
strategy might reach success in fewer steps.

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