Re: TypeFamilies vs. FunctionalDependencies & type-level recursion

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
23 messages Options
12
Reply | Threaded
Open this post in threaded view
|

Re: TypeFamilies vs. FunctionalDependencies & type-level recursion

AntC
>
> Sorry for the late reply.
Thanks Oleg, I take it the Northern hemisphere is now on
academic summer holidays.

>
> [snip]
>
> > Finally, I still think most of the "magic" in everything
> > we've been talking about boils down to being able to
> > have a type variable that can take on any type *except*
> > a certain handful.  This would allow us to avoid
> > overlapping instances of both classes and type families,
> would allow us to define TypeEq, etc.  Moreover, it would
> > be a more direct expression of what programmers intend,
> > and so make code easier to read.  Such a constraint
> cannot be part of the context, because
>
> Alas, such `type variables' with inequality constraints
> are quite complex, and the consequences of their
> introduction are murky. Let me illustrate. First of all,
> the constraint /~ (to be used as t1 /~ Int) doesn't help
> to define TypeEq, etc. because constraints are not used
> when selecting an instance. ...

Yes indeed we can't use constraints when selecting an
instance,
several posters have pointed this out.
I've suggested we call these inequality 'restraints' rather
than 'constraints'.
And a different syntax has been proposed, similar to pattern
guards:
      type instance TypeEq a b   | a /~ b   = HTrue

> Instances are selected only by
> matching a type to the instance head. Instance selection
> based on constraints is quite a change in the type checker
> , and is unlikely to be implemented.

I agree that selecting instances based on constraints would
be abig change, but ...

Selecting instances based on inequalities is already
implemented in GHC and Hugs.
(And has been successfully used for over a decade.) You've
used it extensively yourself in the HList work, and much
other type-level manipulation (such as IsFunction).

Unfortunately, it's not called 'instance selection based on
inequalities' (or some such), and its implementation got all
mixed up with Functional Dependencies, which to my mind is
an orthogonal part of the design.

Instance selection based on inequalities is called
'Overlapping Instances'.
The difficulty in adopting it into Haskell prime is that it
isn't thoroughly specified,
and you can currently only use it with FunDeps.

To avoid confusion with FunDeps, let's imagine we could use
overlapping instances
 with Type Families:
       type family HMember e l
       type instance HMember a HNil         = HFalse
       type instance HMember a (HCons a l') = HTrue
       type instance HMember a (HCons b l') = HMember a l'
Selecting that last instance implies a /~ b.
(Otherwise the HTrue instance would be selected).
Using inequality restraints, we'd write that last instance
as:
       type instance HMember a (HCons b l') | a /~ b =
HMember a l'

And by putting an explicit inequality we are in fact
avoiding the trouble with
overlaps and all their implicit logic:
  The compiler can check that although the instance heads do
overlap,
     the inequality disambiguates the instances.
  So type inference could only select one instance at most.

I think this could be implemented under the new OutsideIn(X)
type inference:
   Inference for the ordinary instances proceeds as usual.
   Inequalities give rise to implication terms(as used for
GADTs),
      with the inequality in the antecedent:
       (a /~ b) implies (TypeEq a b ~ HFalse)
   As with GADTs, inference needs evidence that a /~ b
before applying the consequent.
   There is no danger of clashing with other instances of
TypeEq,
      because the instance (including inequality) doesn't
overlap any of them.

(I made some long posts to the Haskell-prime list last
month, explaining in more detail, and responding to your
TTypeable suggestion.)


>
> _______________________________________________
> Haskell-prime mailing list
> [hidden email]
> http://www.haskell.org/mailman/listinfo/haskell-prime

_______________________________________________
Haskell-prime mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-prime
Reply | Threaded
Open this post in threaded view
|

Re: TypeFamilies vs. FunctionalDependencies & type-level recursion

oleg-30

Let me see if I understand the different points of view. You advocate
keeping Overlapping Instances, with changes to instance resolution
algorithm. I advocate abolishing Overlapping Instances,
claiming it results in no loss of expressiveness. In my approach, the
changes in GHC are minor (essentially bug fixing and a matter of
pretty-printing), not involving the algorithms of instance
resolution. Incidentally, I have advocated abolishing Overlapping
Instances in a short presentation at the 2004 Haskell Workshop (almost
immediately after Ralf's HList talk).

> Selecting instances based on inequalities is already implemented in
> GHC and Hugs.  (And has been successfully used for over a decade.)
> You've used it extensively yourself in the HList work, and much other
> type-level manipulation (such as IsFunction).

I'm glad you mentioned Hugs. Indeed, Hugs implements overlapping
instances, and indeed _some_, simple code using overlapping
instances work the same way in GHC and Hugs. However, HList in
full does not work in Hugs; while investigating the matter we have
found many dark corners of the Overlapping Instances
implementation in Hugs; Ralf has even found an example where the order of
the constraints within a type mattered. After that we just abandoned
Hugs. This fact constructively proves that implementation of
overlapping instances is tricky; since there is no meta-theory, it is
even hard to tell what is right.

I don't think Overlapping Instances will be in Haskell' any time soon
since there are doubts about the soundness. Overlapping
instances are clearly unsound with type functions. Whether they are
sound with functional dependencies is not clear, but there are warning
signs:

        http://www.haskell.org/pipermail/haskell-cafe/2010-July/080043.html

Please see the whole discussion on Haskell-Cafe in July 2010.

> I think this could be implemented under the new OutsideIn(X)
> type inference:
I should point out the need to extend the type inference algorithm
(and prove that the extension is sound) on your point of view. My
proposal does not affect the instance resolution algorithm at all.


> I take it the Northern hemisphere is now on academic summer holidays.
Generally, yes. I wish I had a holiday though...


_______________________________________________
Haskell-prime mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-prime
Reply | Threaded
Open this post in threaded view
|

RE: TypeFamilies vs. FunctionalDependencies & type-level recursion

Simon Peyton Jones
Friends

This has been an interesting thread, but I've been on holiday, and been busy bug-fixing etc, so my cache is very cold.  Moreover, I remember that there was much of it that I wasn't following anyway.  It's tricky.

So, let me ask: does anyone (eg Oleg) have concrete proposals on the table for things they'd like GHC to do?  

Arising from the thread, two particular things jump out at me.  I'm not planning to do anything immediate about either of them.

1.  Support for type representations.  Oleg showed this:

| I have implemented type-level TYPEREP (along with a small library for higher-order
| functional programming at the type level).  Overlapping instances may indeed be
| avoided. The library does not use functional dependencies either.
|
| http://okmij.org/ftp/Haskell/TTypeable/

Yesterday, Brent, Stephanie, Dimitrios, Julien and I were talking about better support for type reps too, something like a better Typeable class:
        class BetterTypeable a where
          typeOf :: Proxy a -> BetterTypeRep a
        data Proxy a
The "better" part is that
        - Both BetterTypeable and Proxy could be poly-kinded, so we didn't need
          Typeable1, Typeable2 etc
        - BetterTypeRep is type-indexed (unlike the current TypeRep)

But BetterTypeRep is still a value-level thing.  You want a type-level type representation, for reasons I don't yet understand.

In any case, *some* built in support for getting at type reps seems reasonable; the question is exactly what.


2. Support for overlapping type function equations.  

There seems no reason in principle to disallow
        type instance F where
          F Int = Bool
          F a = [a]
There is overlap, but it is resolved top-to-bottom.  The only real difficulty with this is how to render it into FC.  The only decent way seems to me to be to allow FC axioms to do pattern matching themselves.  So the FC rendering might be
        ax32 a = case a of
                  Int -> F Int ~ Bool
                  _   -> F a ~ [a]
That is, the axioms become type-indexed.  I don't know what complications that would add.


Simon


| -----Original Message-----
| From: [hidden email] [mailto:[hidden email]] On
| Behalf Of [hidden email]
| Sent: 28 July 2011 06:28
| To: [hidden email]
| Cc: [hidden email]; haskell-
| [hidden email]
| Subject: Re: TypeFamilies vs. FunctionalDependencies & type-level recursion
|
|
| Let me see if I understand the different points of view. You advocate
| keeping Overlapping Instances, with changes to instance resolution
| algorithm. I advocate abolishing Overlapping Instances,
| claiming it results in no loss of expressiveness. In my approach, the
| changes in GHC are minor (essentially bug fixing and a matter of
| pretty-printing), not involving the algorithms of instance
| resolution. Incidentally, I have advocated abolishing Overlapping
| Instances in a short presentation at the 2004 Haskell Workshop (almost
| immediately after Ralf's HList talk).
|
| > Selecting instances based on inequalities is already implemented in
| > GHC and Hugs.  (And has been successfully used for over a decade.)
| > You've used it extensively yourself in the HList work, and much other
| > type-level manipulation (such as IsFunction).
|
| I'm glad you mentioned Hugs. Indeed, Hugs implements overlapping
| instances, and indeed _some_, simple code using overlapping
| instances work the same way in GHC and Hugs. However, HList in
| full does not work in Hugs; while investigating the matter we have
| found many dark corners of the Overlapping Instances
| implementation in Hugs; Ralf has even found an example where the order of
| the constraints within a type mattered. After that we just abandoned
| Hugs. This fact constructively proves that implementation of
| overlapping instances is tricky; since there is no meta-theory, it is
| even hard to tell what is right.
|
| I don't think Overlapping Instances will be in Haskell' any time soon
| since there are doubts about the soundness. Overlapping
| instances are clearly unsound with type functions. Whether they are
| sound with functional dependencies is not clear, but there are warning
| signs:
|
| http://www.haskell.org/pipermail/haskell-cafe/2010-July/080043.html
|
| Please see the whole discussion on Haskell-Cafe in July 2010.
|
| > I think this could be implemented under the new OutsideIn(X)
| > type inference:
| I should point out the need to extend the type inference algorithm
| (and prove that the extension is sound) on your point of view. My
| proposal does not affect the instance resolution algorithm at all.
|
|
| > I take it the Northern hemisphere is now on academic summer holidays.
| Generally, yes. I wish I had a holiday though...
|
|
| _______________________________________________
| Haskell-prime mailing list
| [hidden email]
| http://www.haskell.org/mailman/listinfo/haskell-prime


_______________________________________________
Haskell-prime mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-prime
Reply | Threaded
Open this post in threaded view
|

Re: TypeFamilies vs. FunctionalDependencies & type-level recursion

oleg-30

> But BetterTypeRep is still a value-level thing.  You want a type-level
> type representation, for reasons I don't yet understand.
>
> 2. Support for overlapping type function equations.

I'd like to have type-level type representations to _implement_
overlapping type function equations. With type level Typeable, you
would not need to do anything about point 2 therefore. The problem 2
will be solved.

> There seems no reason in principle to disallow
> type instance F where
>  F Int = Bool
>  F a = [a]


I would implement this as follows:

> type instance F x = F' (EQ (TYPEOF x) INT) x
> type family F' trep x
> type instance F' TRUE  x = Bool
> type instance F' FALSE x = [x]


Furthermore, type-level Typeable is possible already, although in
quite an ugly way: your can read INT as a Peano numeral, and EQ as
Peano numeral equality. In fact, I have demonstrated such an
implementation (even more complex case, for higher-kinds):
        http://okmij.org/ftp/Haskell/TTypeable/


> That is, the axioms become type-indexed.  I don't know what
> complications that would add.

With TTypeable, none of that would be needed. Overlapping Instances
just become redundant.


> So, let me ask: does anyone (eg Oleg) have concrete proposals on the
> table for things they'd like GHC to do?

First of all, can something be done about the behavior reported by
David and discussed in the first part of the message

   http://www.haskell.org/pipermail/haskell-prime/2011-July/003489.html

That is, if *no* undecidable instances are used, the type checker
should reduce type functions for as long as needed. No context
restrictions should be used.

Second, what is the status of Nat kinds and other type-level data that
Conor was/is working on? Nat kinds and optimized comparison of Nat
kinds would be most welcome. Type level lists are better still
(relieving us from Goedel-encoding type representations).

Would it be possible to add TYPEREP (type-level type representation)
as a kind, similar to that of natural numbers and booleans?

Finally, could GHC automatically derive instances of TTypeable, which
maps types to TYPEREP:
        type family TTypeable (x :: *) :: TYPEREP

        Cheers,
        Oleg

_______________________________________________
Haskell-prime mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-prime
Reply | Threaded
Open this post in threaded view
|

Re: TypeFamilies vs. FunctionalDependencies & type-level recursion

Iavor Diatchki
Helllo,

On Sat, Jul 30, 2011 at 2:11 AM, <[hidden email]> wrote:

Second, what is the status of Nat kinds and other type-level data that
Conor was/is working on? Nat kinds and optimized comparison of Nat
kinds would be most welcome. Type level lists are better still
(relieving us from Goedel-encoding type representations).


I  did some work on adding a Nat kind to GHC, you can find the implementation in the "type-nats" branch of GHC.   The code there introduces a new kind, Nat, and it allows you to write natural numbers in types, using singleton types to link them to the value level.  The constraint solver for the type level naturals in that implementation is a bit flaky, so lately I have been working on an improved decision procedure.  When ready, I hope that the new solver should support more operations, and it should be much easier to make it construct explicit proof objects (e.g., in the style of System FC).
-Iavor
PS: I am going on vacation next week, so I'll probably not make much progress on the new solver in August.

_______________________________________________
Haskell-prime mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-prime
Reply | Threaded
Open this post in threaded view
|

Re: TypeFamilies vs. FunctionalDependencies & type-level recursion

Dan Knapp
By the way, I have been testing your type-nats branch this week.  I
added my observations to the
GHC trac ticket on the feature, as you probably saw.  After a
discussion with other people here at
HacPhi, I've decided that what I'm going to attempt is to add
type-level Maybes so that subtraction
and other partial operations can exist.  This entails adding Maybe as
an arity-1 kind constructor,
which of course means adding the notion of kind constructors that have
nonzero arities at all.

On Sat, Jul 30, 2011 at 1:55 PM, Iavor Diatchki
<[hidden email]> wrote:

> Helllo,
>
> On Sat, Jul 30, 2011 at 2:11 AM, <[hidden email]> wrote:
>>
>> Second, what is the status of Nat kinds and other type-level data that
>> Conor was/is working on? Nat kinds and optimized comparison of Nat
>> kinds would be most welcome. Type level lists are better still
>> (relieving us from Goedel-encoding type representations).
>>
>
> I  did some work on adding a Nat kind to GHC, you can find the
> implementation in the "type-nats" branch of GHC.   The code there introduces
> a new kind, Nat, and it allows you to write natural numbers in types, using
> singleton types to link them to the value level.  The constraint solver for
> the type level naturals in that implementation is a bit flaky, so lately I
> have been working on an improved decision procedure.  When ready, I hope
> that the new solver should support more operations, and it should be much
> easier to make it construct explicit proof objects (e.g., in the style of
> System FC).
> -Iavor
> PS: I am going on vacation next week, so I'll probably not make much
> progress on the new solver in August.
> _______________________________________________
> Haskell-prime mailing list
> [hidden email]
> http://www.haskell.org/mailman/listinfo/haskell-prime
>
>



--
Dan Knapp
"An infallible method of conciliating a tiger is to allow oneself to
be devoured." (Konrad Adenauer)

_______________________________________________
Haskell-prime mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-prime
Reply | Threaded
Open this post in threaded view
|

RE: TypeFamilies vs. FunctionalDependencies & type-level recursion

Simon Peyton Jones
| GHC trac ticket on the feature, as you probably saw.  After a
| discussion with other people here at
| HacPhi, I've decided that what I'm going to attempt is to add
| type-level Maybes

Hang on!  Julien Cretin (from INRIA) is doing an internship here at Cambridge with Dimitrios and me.  The primary goal is to support *typed* type-level programming; that is, to add a proper kind system to GHC.

Broadly our approach is like Conor's SHE system, with minor syntactic differences.  So type-level Maybes will appear automatically, as a special case, so it's probably a bit of a waste to implement them separately.  

There'll also be support for poly-kinded type-level functions, of course.

The stuff will be on a branch in the main ghc repo soon.

Julien: we should start a wiki page (see http://hackage.haskell.org/trac/ghc/wiki/Commentary, and look for the link to "Type level naturals"; one like that).  On the wiki you should
 * add a link to the latest version of our (evolving) design document.
 * specify the branch in the repo that has the stuff
 * describe the status

Iavor's stuff is still highly relevant, because it involves a special-purpose constraint solver.  But Iavor's stuff is no integrated into HEAD, and we need to talk about how to do that, once you are back from holiday Iavor.

Simon

_______________________________________________
Haskell-prime mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-prime
Reply | Threaded
Open this post in threaded view
|

RE: TypeFamilies vs. FunctionalDependencies & type-level recursion

Simon Peyton Jones
In reply to this post by oleg-30
Oleg

| > There seems no reason in principle to disallow
| > type instance F where
| >  F Int = Bool
| >  F a = [a]
|
|
| I would implement this as follows:
|
| > type instance F x = F' (EQ (TYPEOF x) INT) x
| > type family F' trep x
| > type instance F' TRUE  x = Bool
| > type instance F' FALSE x = [x]

But you have just pushed the problem off to the definition of EQ.  And your definition of EQ requires a finite enumeration of all types, I think.  But * is open, so that's hard to do. What you want is
   type instance EQ where
       EQ a a = TRUE
       EQ _ _ = FALSE
and now we are back where we started.

Moreover, encoding the negative conditions that turn an arbitrary collection of equations with a top-to-bottom reading into a set of independent equations, is pretty tedious.

| First of all, can something be done about the behavior reported by
| David and discussed in the first part of the message
|
|    http://www.haskell.org/pipermail/haskell-prime/2011-July/003489.html

OK.  Can you give a small standalone test case to demonstrate the problem, and open a Track ticket for it?

| Second, what is the status of Nat kinds and other type-level data that
| Conor was/is working on?

Julien is working hard on an implementation right now.  The Wiki page is here
        http://hackage.haskell.org/trac/ghc/wiki/GhcKinds
Attached there are documents describing what we are up to.

| Would it be possible to add TYPEREP (type-level type representation)
| as a kind, similar to that of natural numbers and booleans?

Yes!  See 5.4 of "the theory document". It's still very incoherent, but it's coming along.

Simon


_______________________________________________
Haskell-prime mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-prime
Reply | Threaded
Open this post in threaded view
|

Re: TypeFamilies vs. FunctionalDependencies & type-level recursion

oleg-30


> But you have just pushed the problem off to the definition of EQ.  And
> your definition of EQ requires a finite enumeration of all types, I
> think.  But * is open, so that's hard to do. What you want is
>    type instance EQ where
>        EQ a a = TRUE
>        EQ _ _ = FALSE
> and now we are back where we started.

Not at all. In the first approximation, EQ is the _numerical_
equality, equality of two type-level naturals. Since Goedel numbering
is no fun in practice, I agree on the second approximation, described
in TTypeable.hs. I quote the beginning of that file for reference:

> module TTypeable where
> {-
>  It helps in understanding the code if we imagine Haskell had
>  algebraic data kinds. We could then say
>
> kind TyCon_name -- name associated with each (registered) type constructor
>
> kind NAT        -- Type-level natural numbers
> kind BOOL       -- Type-level booleans
>
> kind LIST a = NIL | a :/ LIST a
>
> -- Type-level type representation
> kind TYPEREP = (TyCon_name, LIST TYPEREP)
> -}
>
> -- Type-lever typeOf
> -- The more precise kind is * -> TYPEREP
> type family TYPEOF ty :: *
>
> -- Auxiliary families
>
> -- The more precise kind is TyCon_name -> NAT
> type family TC_code tycon :: *
>
> -- Sample type reps (the rest should be derived, using TH, for example)
> -- Alternatively, it would be great if GHC could provide such instances
> -- automatically or by demand, e.g.,
> -- deriving instance TYPEOF Foo

> data TRN_unit
> type instance TC_code TRN_unit = Z
> type instance TYPEOF () = (TRN_unit, NIL)

> data TRN_bool
> type instance TC_code TRN_bool = S Z
> type instance TYPEOF Bool = (TRN_bool, NIL)

I could write a TH function tderive to be used as follows. When the
user defines a new data type

data Foo = ...

then $(tderive ''Foo)

expands in

> data TRN_package_name_module_name_Foo
> type instance TC_code TRN_package_name_module_name_Foo =
>  <very long type-level numeral that spells package_name_module_name_Foo in unary>
> type instance TYPEOF Foo = (TRN_package_name_module_name_Foo, NIL)


I think I can write such tderive right now. So, the EQ (or, TREPEQ as
I call it) is defined in closed form:

> -- Comparison predicate on TYPEREP and its parts
>
> -- TYPEREP -> TYPEREP -> BOOL
> type family TREPEQ x y :: *
>
> type instance TREPEQ (tc1, targ1) (tc2, targ2) =
>     AND (NatEq (TC_code tc1) (TC_code tc2))
> (TREPEQL targ1 targ2)
>
> -- LIST TYPEREP -> LIST TYPEREP -> BOOL
> type family TREPEQL xs ys :: *
>
> type instance TREPEQL NIL NIL      = HTrue
> type instance TREPEQL NIL (h :/ t) = HFalse
> type instance TREPEQL (h :/ t) NIL = HFalse
> type instance TREPEQL (h1 :/ t1) (h2 :/ t2) =
>     AND (TREPEQ h1 h2) (TREPEQL t1 t2)

That is it. These are the all clauses. Again, I have already defined
them, and it works in GHC 7.0. Certainly I would be grateful if GHC
blessed them with a special attention so they run faster.


_______________________________________________
Haskell-prime mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-prime
Reply | Threaded
Open this post in threaded view
|

Re: TypeFamilies vs. FunctionalDependencies & type-level recursion

Iavor Diatchki
In reply to this post by Simon Peyton Jones
Hello,

On Tue, Aug 2, 2011 at 6:10 PM, Simon Peyton-Jones
<[hidden email]> wrote:
> Julien: we should start a wiki page (see http://hackage.haskell.org/trac/ghc/wiki/Commentary, and look for the link to "Type level naturals"; one like that).  On the wiki you should
>  * add a link to the latest version of our (evolving) design document.
>  * specify the branch in the repo that has the stuff
>  * describe the status

Yes, this would be quite useful!

> Iavor's stuff is still highly relevant, because it involves a special-purpose constraint solver.  But Iavor's stuff is no integrated into HEAD, and we need to talk about how to do that, once you are back from holiday Iavor.

I'll send an e-mail to the list when I'm back.  I think I've made
quite a bit of progress on the solver, and I've been working on a
document (actually a literate Haskell file) which explains how it
works and also my understanding of GHC's constraint solver that I'd be
very happy to get some feedback on.

-Iavor

_______________________________________________
Haskell-prime mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-prime
Reply | Threaded
Open this post in threaded view
|

Re: TypeFamilies vs. FunctionalDependencies & type-level recursion

AntC
In reply to this post by oleg-30
 <oleg@...> writes:
>
>
> [28 Jul 2011] ... . Incidentally, I have advocated abolishing Overlapping
> Instances in a short presentation at the 2004 Haskell Workshop (almost
> immediately after Ralf's HList talk).

Hi Oleg, I appreciate it's been a very long time since this thread was active.
But I think I might have discovered that you and Ralf were premature to reject
overlaps w.r.t. HList.

The headline news is that I have implemented hDeleteMany in Hugs.

I'm dragging up this ancient history not to argue in favour of fundeps, nor to
bring Hugs back from its slumbers, but pro a better-implemented approach to
overlaps (preferably available with Type Families).

To recap the context:

>
> > [AntC wrote]
> > Selecting instances based on inequalities is already implemented in
> > GHC and Hugs.  (And has been successfully used for over a decade.)
> > You've used it extensively yourself in the HList work, and much other
> > type-level manipulation (such as IsFunction).
Also the original post said:
> > Selecting instances based on inequalities ... got all mixed up with
> > Functional Dependencies ...
>
> I'm glad you mentioned Hugs. Indeed, Hugs implements overlapping
> instances, and indeed _some_, simple code using overlapping
> instances work the same way in GHC and Hugs. However, HList in
> full does not work in Hugs; ...

The point at which the HList paper "give up on persuading Hugs" was with the
instance definitions for hDeleteMany [Section 6 'Ended up in murky water']
because "There is no real consensus on the overlapping instance mechanism as
soon as functional dependencies are involved. ... Hugs reports that the
instances are inconsistent with the functional dependency for HDeleteMany."

There has been a lot of water under the bridge since that interchange. In
particular, GHC has got type equality constraints mature, with powerful type
inference. SPJ showed a technique he called "a functional-dependency-like
mechanism (but using equalities) for the result type". [This was for an
application where using an Associated Type would not work. So he introduced an
extra type parameter to the class.]

I noted that HList has an approximation to equality constraints (TypeCast). I
took the fundep away from HDeleteMany, and instead implemented the instances
with TypeCast constraints to infer the result type:
1. There's no longer trouble with fundep interference.
2. So you can declare the instances OK (with overlaps well-ordered).
3. The typecast works a dream.

[To be precise, I haven't done away with fundeps altogether, because they
support TypeCast. And I expect that hDeleteMany without fundeps is not going
to play well with large-scale programs needing extensive type inference. My
point is only that it's the interference between fundeps and overlap that
messes up both.]

We could possibly design a better fundep, but I think fundeps are moribund.
I'd rather put the effort into introducing overlaps into Type Families, and
addressing the soundness concerns.

>
> I don't think Overlapping Instances will be in Haskell' any time soon
> since there are doubts about the soundness. Overlapping
> instances are clearly unsound with type functions. Whether they are
> sound with functional dependencies is not clear, but there are warning
> signs:
>
> http://www.haskell.org/pipermail/haskell-cafe/2010-July/080043.html
>
> Please see the whole discussion on Haskell-Cafe in July 2010.
>

I have now studied SPJ's post, and that whole discussion. [Heck, July 2010 had
some heavy-duty type theory.] I note that one of the threads that month was
on 'in-equality type constraint's -- which is exactly what I think it needs to
handle overlapping instances in a disciplined way.  SPJ's post is dense, and I
think worth replying to in detail, now that we have mature experience with
equality constraints.

>
> > I take it the Northern hemisphere is now on academic summer holidays.
> Generally, yes. I wish I had a holiday though...
>
My timing is again terrible: I suppose Northern Hemisphere academics are
furiously ending their year and heading for the beach.

AntC


_______________________________________________
Haskell-prime mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-prime
Reply | Threaded
Open this post in threaded view
|

Re: TypeFamilies vs. FunctionalDependencies & type-level recursion

AntC
AntC <anthony_clayden@...> writes:

>
>  <oleg@...> writes:
> >
>
> The headline news is that I have implemented hDeleteMany in Hugs.
>

Yikes! I'd better post the code. This assumes all the usual HList
infrastructure, especially class/method TypeCast as defined in-line per  
http://okmij.org/ftp/Haskell/typecast.html

Works on Hugs version Sep 2006 -- yes! it's been hiding in plain view all
these years.

{- hDeleteMany does a type-indexed scan through an HList,
        removing all elements type `e`, even if they occur many times.
        Takes the standard HList idiom of 3 instances:
        - end of HList -- contains only HNil
        - HList's head contains the element of interest (HCons e l'')
        - HList's head not interesting, pass on (HCons e' l'')
        The 'interesting' instance overlaps the 'not interesting'.
-}

    class HDeleteMany e l l' where -- no fundep
        hDeleteMany :: e -> l -> l'

    instance (TypeCast HNil l') => HDeleteMany e HNil l' where
        hDeleteMany e HNil = typeCast HNil
                            -- must typeCast the result

    instance (HDeleteMany e l'' l') => HDeleteMany e (HCons e l'') l'  where
        hDeleteMany e (HCons _ l'') = hDeleteMany e l''

    instance (HDeleteMany e l'' l''', TypeCast (HCons e' l''') l')
         => HDeleteMany e (HCons e' l'') l'                where
            hDeleteMany e (HCons e' l'') = typeCast (HCons e' (hDeleteMany e
l''))
-- tests:
    somelist = HCons True $ HCons 'H' $ HCons "HList" $ HCons (5 :: Int)
HNil
    somemanylist = HCons "hello" $ HCons False somelist

    unmanylist = hDeleteMany "bye" (hDeleteMany (undefined :: Bool)
somemanylist )
-- unmanylist ===> HCons 'H' (HCons 5 HNil)


AntC





_______________________________________________
Haskell-prime mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-prime
Reply | Threaded
Open this post in threaded view
|

Re: TypeFamilies vs. FunctionalDependencies & type-level recursion

AntC
In reply to this post by Simon Peyton Jones
Simon Peyton-Jones <simonpj@...> writes:

> [from 29 Jul 2011]
>
> So, let me ask: does anyone (eg Oleg) have concrete proposals on the table
for things they'd like GHC to do?  
>
> Arising from the thread, two particular things jump out at me.  ...

The two things are, I think, trying to achieve the same objective. Namely,
supporting type-level inference driven from a type-level equality predicate.

Of those two things (details continued below), I understand Oleg does have a
concrete proposal for the first (and a prototype). My proposal earlier in the
thread was along the lines of your second particular thing. But I delayed
replying immediately:
- Oleg suggested I refer back to several similar threads in July 2010
        (thank you, that was indeed a valuable discussion)
- GHC has now delivered robust type inference with type equality constraints,
- and superclass constraints.
- And we have the beginnings of data Kinds
- And there has been 'loose talk' of closed Kinds

(To explain that last: I believe the type inference for closed Kinds will need
a similar mechanism to overlapping instances for TypeFamilies.)

Although this thread is titled FunctionalDependencies, I'm not going to say
anything about them except that they interfere badly with overlaps, so both
have got an unfair reputation IMHO.

Thanks to the improvements in type inference, SPJ has shown a technique he
called "a functional-dependency-like mechanism (but using equalities) for the
result type". That applies for Type Class instances, and GHC supports
overlapping for those, so I've used the technique to simulate overlapping
TypeFamily instances.
 

>
> 1.  Support for type representations.  Oleg showed this:
>
> | I have implemented type-level TYPEREP ...
>
>
> 2. Support for overlapping type function equations.  
>
> There seems no reason in principle to disallow
> type instance F where
>  F Int = Bool
>  F a = [a]
> There is overlap, but it is resolved top-to-bottom.  The only real
difficulty with this is how to render it
> into FC.  The only decent way seems to me to be to allow FC axioms to do
pattern matching themselves.  So the FC
> rendering might be
> ax32 a = case a of
>                   Int -> F Int ~ Bool
>                   _   -> F a ~ [a]
> That is, the axioms become type-indexed.  I don't know what complications
that would add.
>

I favour support for overlapping type function equations, but not exactly that
approach. I think a major complication from the programmer's point of view is
that the type function equations would have to be declared all in the same
place. (I suspect there would be a similar restriction with closed Kinds.)

A complication for type inference is carrying around some representation of
that case statement, and applying the top-to-bottom inference.

I think it preferable from a programmer's point of view to have separately
declared stand-alone instances. And I guess this might be easier to manage for
type inference.

And I propose a form for the instances that achieves the type function above,
but with what you might call "explicitly non-overlapping overlaps", like this:

        type instance F Int = Bool
        type instance F a | a /~ Int = [a]  -- explicit dis-equality restraint

These can't overlap, because the restraint (aka type-level guard) says "you
must have evidence that typevar a is not Int before this binding applies". And
we can validate those instances for non-overlap: the instance heads overlap
just in case a ~ Int. (I suspect much of this logic is already in place to
handle overlapping instances. In a 2010 post Oleg gave a very convincing
characterisation.)

[Something very similar to dis-equality guards was briefly shown in Sulzmann &
Stuckey. A Theory of Overloading (2002).]

I'm calling these "restraints" because they're not like constraints.
Restraints block instance matching, whereas constraints validate the instance
_after_ matching. But the terminology is going to get confusing, because
inside type inference, I think they'd be implemented as what's
called "implication constraints" (as used for GADT's).

That second binding gives rise to an axiom:

        (a /~ Int ==> F a ~ [a])    -- using ==> for implication

(The axiom for the first binding is as usual, no implication needed.)


I dislike Oleg's TypeRep approach, because it brings in another layer of
encoding. I think it would be simpler from a programmer's point of view to
have types 'standing for themselves'.

I prefer "explicitly non-overlapping overlaps" because the type function
guards look and behave similarly to guards for function bindings. (But a
significant difference is that type function instances must be mutually
exclusive, and that's how come they can be declared stand-alone. The
requirement to be mutually exclusive means we avoid all that trouble with
IncoherentInstances and imported overlaps silently changing behaviour -- I
would explain further, but this post has gone on long enough.)

AntC




_______________________________________________
Haskell-prime mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-prime
Reply | Threaded
Open this post in threaded view
|

Re: TypeFamilies vs. FunctionalDependencies & type-level recursion

AntC
In reply to this post by oleg-30
 <oleg@...> writes:

> I'd like to have type-level type representations to _implement_
> overlapping type function equations. With type level Typeable, you
> would not need to do anything about point 2 therefore. The problem 2
> will be solved.
>
> > There seems no reason in principle to disallow
> > type instance F where
> >  F Int = Bool
> >  F a = [a]
>
> I would implement this as follows:
>
> > type instance F x = F' (EQ (TYPEOF x) INT) x
> > type family F' trep x
> > type instance F' TRUE  x = Bool
> > type instance F' FALSE x = [x]
>

Thanks Oleg. I'm familiar with that style from HList, but it still seems
cumbersome to me (compared to separate equations). I suppose a type-level if-
then-else would be possible? Does this read any better?

    type instance F x = IF (EQ (TYPEOF x) INT) Bool [x]

I note there by the way, that INT ~ (TYPEOF Int), is that upshifting the name
going to work well for all Prelude types?
    How about (TYPEOF ()) or (TYPEOF [a])?
The EQ seems somehow redundant. We can only test type (reps) for equality, or
do you envisage inducing some ordering over typereps?

How scalable is your approach with multi-argument type functions? Such as:

    module Mine where
      type family F a b

      data Mine = ...
      type instance F Mine Int = ...
      type instance F Mine y   = ...          -- overlap on 2nd arg

    module Yours where
      import Mine

      data Yours = ...
      type instance F Yours Bool = ...         -- no overlap with F Mine b
      type instance F Yours y   = ...          -- overlap on 2nd arg

We'd need a clan of helper functions F'Mine, F'Yours, etc.

This multi-argument example also goes against closed type families, I think.


>
> Finally, could GHC automatically derive instances of TTypeable, which
> maps types to TYPEREP:
> type family TTypeable (x :: *) :: TYPEREP
>

I can see that if we went the route of type-level Typeable, it would need
compiler support. But do we need that? Would it be sufficient to have a
compiler-supported if-then-else type equality? Perhaps IFEQ, like this:

    type instance F a = IFEQ a Int Bool [a]
    type instance F a = (a ?~ Int) Bool [a]     -- over-exotic syntax?

To be fair to the design you've put into TTypeable, we'd also need to handle
polymorphic/partly-ground/higher-ranked types:

    type instance G a          = IFEQ a (Maybe b) b ()
    type instance IsFunction a = IFEQ a (_ -> _) TRUE FALSE   -- the classic
    type instance IsNum a      = IFEQ a (Num b => b) a Int

And that last example is a worry: what we're calling a type equality test is
really a test for unifiability.

AntC




_______________________________________________
Haskell-prime mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-prime
Reply | Threaded
Open this post in threaded view
|

Re: TypeFamilies vs. FunctionalDependencies & type-level recursion

AntC
In reply to this post by oleg-30
 <oleg@...> writes:

>
>
> I don't think Overlapping Instances will be in Haskell' any time soon
> since there are doubts about the soundness. Overlapping
> instances are clearly unsound with type functions. Whether they are
> sound with functional dependencies is not clear, but there are warning
> signs:
>
> http://www.haskell.org/pipermail/haskell-cafe/2010-July/080043.html
>
I have now worked through that post in detail, thank you. And replied (on the
cafe http://www.haskell.org/pipermail/haskell-cafe/2012-May/101417.html )

As SPJ says there, I don't expect there's any real difference in the fundeps
approach compared to type families. And as a matter of taste, I find type
families more easy to understand and reason about, and more *functional*.

But I don't see in SPJ's post any real doubts about soundness, just
restrictions that would have to be imposed. He concludes "I believe that
if ..., then overlap of type families would be fine."

The only onerous restriction is that overlapping instances would have to be in
a single module. And I don't think that is needed under my proposal to dis-
overlap overlaps.

As a matter of interest, how would the TTypeable approach address those
examples? Particularly the existentials (examples 3 and 4). How would it look
inside the GADTs to discharge the constraints (or apply the type functions)?

I notice example 4 (and 1) 'exploits' separate compilation/imported
overlapping instances to arrive at unsoundness. How does TTypeable handle
imported instances?

AntC



_______________________________________________
Haskell-prime mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-prime
Reply | Threaded
Open this post in threaded view
|

RE: TypeFamilies vs. FunctionalDependencies & type-level recursion

Simon Peyton Jones
See also http://hackage.haskell.org/trac/ghc/wiki/NewAxioms
(as yet unimplemented)

Simon

| -----Original Message-----
| From: [hidden email] [mailto:haskell-prime-
| [hidden email]] On Behalf Of AntC
| Sent: 24 May 2012 14:00
| To: [hidden email]
| Subject: Re: TypeFamilies vs. FunctionalDependencies & type-level
| recursion
|
|  <oleg@...> writes:
|
| >
| >
| > I don't think Overlapping Instances will be in Haskell' any time soon
| > since there are doubts about the soundness. Overlapping instances are
| > clearly unsound with type functions. Whether they are sound with
| > functional dependencies is not clear, but there are warning
| > signs:
| >
| > http://www.haskell.org/pipermail/haskell-cafe/2010-July/080043.html
| >
| I have now worked through that post in detail, thank you. And replied
| (on the cafe http://www.haskell.org/pipermail/haskell-cafe/2012-
| May/101417.html )
|
| As SPJ says there, I don't expect there's any real difference in the
| fundeps approach compared to type families. And as a matter of taste, I
| find type families more easy to understand and reason about, and more
| *functional*.
|
| But I don't see in SPJ's post any real doubts about soundness, just
| restrictions that would have to be imposed. He concludes "I believe that
| if ..., then overlap of type families would be fine."
|
| The only onerous restriction is that overlapping instances would have to
| be in a single module. And I don't think that is needed under my
| proposal to dis- overlap overlaps.
|
| As a matter of interest, how would the TTypeable approach address those
| examples? Particularly the existentials (examples 3 and 4). How would it
| look inside the GADTs to discharge the constraints (or apply the type
| functions)?
|
| I notice example 4 (and 1) 'exploits' separate compilation/imported
| overlapping instances to arrive at unsoundness. How does TTypeable
| handle imported instances?
|
| AntC
|
|
|
| _______________________________________________
| Haskell-prime mailing list
| [hidden email]
| http://www.haskell.org/mailman/listinfo/haskell-prime



_______________________________________________
Haskell-prime mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-prime
Reply | Threaded
Open this post in threaded view
|

Re: TypeFamilies vs. FunctionalDependencies & type-level recursion

AntC
Simon Peyton-Jones <simonpj@...> writes:

>
> See also http://hackage.haskell.org/trac/ghc/wiki/NewAxioms
> (as yet unimplemented)
>
> Simon
>

Thank you Simon (and Pedro).

Are you inviting comment/suggestions/requests for clarification at this stage?
(Or is this under-the-radar research?)

There is plenty of prior work/similar ideas to include in the references.

How's the best way to help? (Without unleashing a maelstrom.)

AntC



_______________________________________________
Haskell-prime mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-prime
Reply | Threaded
Open this post in threaded view
|

Re: TypeFamilies vs. FunctionalDependencies & type-level recursion

José Pedro Magalhães
Hi,

On Tue, May 29, 2012 at 11:03 AM, AntC <[hidden email]> wrote:
Simon Peyton-Jones <simonpj@...> writes:

>
> See also http://hackage.haskell.org/trac/ghc/wiki/NewAxioms
> (as yet unimplemented)
>
> Simon
>

Thank you Simon (and Pedro).

Are you inviting comment/suggestions/requests for clarification at this stage?

Definitely! I think the design space should be explored in detail.
 
There is plenty of prior work/similar ideas to include in the references.

That document is not a paper draft; it's a draft of a design of a new GHC extension.
 
How's the best way to help? (Without unleashing a maelstrom.)

Perhaps having a wiki page where the problem of OverlappingInstances is discussed, and alternative solutions are proposed, so that at some point we can look at all of them and try to make an informed decision. I think it's good to have a wiki page to guide this sort of email discussion.


Cheers,
Pedro
 

AntC



_______________________________________________
Haskell-prime mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-prime


_______________________________________________
Haskell-prime mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-prime
Reply | Threaded
Open this post in threaded view
|

RE: TypeFamilies vs. FunctionalDependencies & type-level recursion

Simon Peyton Jones

I have expanded the draft spec on

http://hackage.haskell.org/trac/ghc/wiki/NewAxioms

to answer some of the questions on AntC’s discussion page.

 

 

From: [hidden email] [mailto:[hidden email]] On Behalf Of José Pedro Magalhães
Sent: 29 May 2012 11:14
To: AntC
Cc: [hidden email]
Subject: Re: TypeFamilies vs. FunctionalDependencies & type-level recursion

 

Hi,

On Tue, May 29, 2012 at 11:03 AM, AntC <[hidden email]> wrote:

Simon Peyton-Jones <[hidden email]> writes:

>
> See also http://hackage.haskell.org/trac/ghc/wiki/NewAxioms
> (as yet unimplemented)
>
> Simon
>

Thank you Simon (and Pedro).

Are you inviting comment/suggestions/requests for clarification at this stage?


Definitely! I think the design space should be explored in detail.
 

There is plenty of prior work/similar ideas to include in the references.


That document is not a paper draft; it's a draft of a design of a new GHC extension.
 

How's the best way to help? (Without unleashing a maelstrom.)


Perhaps having a wiki page where the problem of OverlappingInstances is discussed, and alternative solutions are proposed, so that at some point we can look at all of them and try to make an informed decision. I think it's good to have a wiki page to guide this sort of email discussion.


Cheers,
Pedro
 


AntC



_______________________________________________
Haskell-prime mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-prime

 


_______________________________________________
Haskell-prime mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-prime
Reply | Threaded
Open this post in threaded view
|

Re: TypeFamilies vs. FunctionalDependencies & type-level recursion

AntC
Simon Peyton-Jones <simonpj@...> writes:

>
> I have expanded the draft spec on
> http://hackage.haskell.org/trac/ghc/wiki/NewAxioms

Thanks Simon, that's much clearer.

By the way, are the examples for the multi- type instance declarations quite
as intended? The heads have no head, as it were. Did you mean, or is this
allowed?

    type instance F [a] where ...

    type instance F (a, b) where ...

(From a documentation point of view, this shows that the instance groups are
non-overlapping.)

> to answer some of the questions on AntC’s discussion page.
>  

(I'd rather you called it just *the* discussion page; I'm doing the ego-less
contributor thing. I must admit that after I got the page started, I've not
had so much time to keep building it.)

AntC


_______________________________________________
Haskell-prime mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-prime
12