Current research on overlapping/closed type families?

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

Current research on overlapping/closed type families?

Ryan Ingram
What's the status of overlapping/closed type families?  I'm interested
in something like the following, which can currently be implemented in
GHC with Oleg-magic using functional dependencies, but cannot, to my
knowledge, be implemented with type families:

data HTrue = HTrue
data HFalse = HFalse

type family IsFunction f

{- not legal in GHC6.10 -}
type instances
   IsFunction (a -> b) = HTrue
   IsFunction a = HFalse

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

RE: Current research on overlapping/closed type families?

Simon Peyton Jones
Provided all the overlapping instances are supplied together, as you suggest, I think what you say makes perfect sense and does not threaten soundness.

But we have not yet implemented the idea yet.  First priority is to get type families working properly, and in conjunction with type classes.  Then we can move on to adding features.

Simon

| -----Original Message-----
| From: [hidden email] [mailto:haskell-cafe-
| [hidden email]] On Behalf Of Ryan Ingram
| Sent: 19 January 2009 23:24
| To: Haskell Cafe
| Subject: [Haskell-cafe] Current research on overlapping/closed type families?
|
| What's the status of overlapping/closed type families?  I'm interested
| in something like the following, which can currently be implemented in
| GHC with Oleg-magic using functional dependencies, but cannot, to my
| knowledge, be implemented with type families:
|
| data HTrue = HTrue
| data HFalse = HFalse
|
| type family IsFunction f
|
| {- not legal in GHC6.10 -}
| type instances
|    IsFunction (a -> b) = HTrue
|    IsFunction a = HFalse
|
|   -- ryan
| _______________________________________________
| Haskell-Cafe mailing list
| [hidden email]
| http://www.haskell.org/mailman/listinfo/haskell-cafe

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

Re: Current research on overlapping/closed type families?

Ryan Ingram
Of course.  I was just wondering if anyone was looking into the
implications of said features :)

For example, with this instance, if "a" is a type variable, you can't
reduce "IsFunction a" to HFalse, because "a" might be "b -> c" for
some b, c.

Whereas in the current formulation, you can treat the declaration as a
rewrite rule without considering how variables are instantiated.  Of
course, this makes IsFunction far less useful; if you were using it
to, for example, define automatic currying and uncurrying of
n-argument functions, it matters whether the result is higher-order or
not, which is somewhat unsatisfying.

  -- ryan

On Fri, Jan 23, 2009 at 6:06 PM, Simon Peyton-Jones
<[hidden email]> wrote:

> Provided all the overlapping instances are supplied together, as you suggest, I think what you say makes perfect sense and does not threaten soundness.
>
> But we have not yet implemented the idea yet.  First priority is to get type families working properly, and in conjunction with type classes.  Then we can move on to adding features.
>
> Simon
>
> | -----Original Message-----
> | From: [hidden email] [mailto:haskell-cafe-
> | [hidden email]] On Behalf Of Ryan Ingram
> | Sent: 19 January 2009 23:24
> | To: Haskell Cafe
> | Subject: [Haskell-cafe] Current research on overlapping/closed type families?
> |
> | What's the status of overlapping/closed type families?  I'm interested
> | in something like the following, which can currently be implemented in
> | GHC with Oleg-magic using functional dependencies, but cannot, to my
> | knowledge, be implemented with type families:
> |
> | data HTrue = HTrue
> | data HFalse = HFalse
> |
> | type family IsFunction f
> |
> | {- not legal in GHC6.10 -}
> | type instances
> |    IsFunction (a -> b) = HTrue
> |    IsFunction a = HFalse
> |
> |   -- ryan
> | _______________________________________________
> | Haskell-Cafe mailing list
> | [hidden email]
> | http://www.haskell.org/mailman/listinfo/haskell-cafe
>
>
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Current research on overlapping/closed type families?

Dan Weston
In reply to this post by Simon Peyton Jones
Would this then also eventually work?

data Zero
data Succ a = Succ a

type family IsFunction f

type instances
   IsFunction (a -> b) = Succ (IsFunction b)
   IsFunction c        = Zero


Simon Peyton-Jones wrote:

> Provided all the overlapping instances are supplied together, as you suggest, I think what you say makes perfect sense and does not threaten soundness.
>
> But we have not yet implemented the idea yet.  First priority is to get type families working properly, and in conjunction with type classes.  Then we can move on to adding features.
>
> Simon
>
> | -----Original Message-----
> | From: [hidden email] [mailto:haskell-cafe-
> | [hidden email]] On Behalf Of Ryan Ingram
> | Sent: 19 January 2009 23:24
> | To: Haskell Cafe
> | Subject: [Haskell-cafe] Current research on overlapping/closed type families?
> |
> | What's the status of overlapping/closed type families?  I'm interested
> | in something like the following, which can currently be implemented in
> | GHC with Oleg-magic using functional dependencies, but cannot, to my
> | knowledge, be implemented with type families:
> |
> | data HTrue = HTrue
> | data HFalse = HFalse
> |
> | type family IsFunction f
> |
> | {- not legal in GHC6.10 -}
> | type instances
> |    IsFunction (a -> b) = HTrue
> |    IsFunction a = HFalse
> |
> |   -- ryan
> | _______________________________________________
> | Haskell-Cafe mailing list
> | [hidden email]
> | http://www.haskell.org/mailman/listinfo/haskell-cafe
>
> _______________________________________________
> Haskell-Cafe mailing list
> [hidden email]
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
>


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

RE: Current research on overlapping/closed type families?

Simon Peyton Jones
| Would this then also eventually work?
|
| data Zero = Zero
| data Succ a = Succ a
|
| type family IsFunction f
|
| type instances
|    IsFunction (a -> b) = Succ (IsFunction b)
|    IsFunction c        = Zero

It's delicate. Consider

        f :: a -> IsFunction a
        f x = Zero

        h = f ord

The defn of f looks ok, but if you were to inline it at the call site, where it's applied to 'ord', which has a functional type, you'll see that 'a' is instantiated by (Char -> Int)...

A similar issue arises with type classes and overlapping instances.  Generally GHC refrains from committing to an instance declaration until it's clear that no other instance can match (in which case the above defn would be rejected).  Maybe the same thing will work for equalities; I have not thought about it.

Simon


|
|
| Simon Peyton-Jones wrote:
| > Provided all the overlapping instances are supplied together, as you
| suggest, I think what you say makes perfect sense and does not threaten
| soundness.
| >
| > But we have not yet implemented the idea yet.  First priority is to
| get type families working properly, and in conjunction with type
| classes.  Then we can move on to adding features.
| >
| > Simon
| >
| > | -----Original Message-----
| > | From: [hidden email] [mailto:haskell-cafe-
| > | [hidden email]] On Behalf Of Ryan Ingram
| > | Sent: 19 January 2009 23:24
| > | To: Haskell Cafe
| > | Subject: [Haskell-cafe] Current research on overlapping/closed type
| families?
| > |
| > | What's the status of overlapping/closed type families?  I'm
| interested
| > | in something like the following, which can currently be implemented
| in
| > | GHC with Oleg-magic using functional dependencies, but cannot, to
| my
| > | knowledge, be implemented with type families:
| > |
| > | data HTrue = HTrue
| > | data HFalse = HFalse
| > |
| > | type family IsFunction f
| > |
| > | {- not legal in GHC6.10 -}
| > | type instances
| > |    IsFunction (a -> b) = HTrue
| > |    IsFunction a = HFalse
| > |
| > |   -- ryan
| > | _______________________________________________
| > | Haskell-Cafe mailing list
| > | [hidden email]
| > | http://www.haskell.org/mailman/listinfo/haskell-cafe
| >
| > _______________________________________________
| > Haskell-Cafe mailing list
| > [hidden email]
| > http://www.haskell.org/mailman/listinfo/haskell-cafe
| >
| >
|

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