Intersection types for Haskell?

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

Intersection types for Haskell?

Brian Hulley
Hi -
I'm wondering if there is any possiblility of getting intersection types
into Haskell. For example, at the moment there is no (proper) typing for:

    f g x y = (g x, g y)

Ideally, I'd like to be able to write:

    f:: (a -> b & c -> d) -> a -> c -> (b,d)

or

    f :: (a -> b a) -> c -> d -> (b c, b d)

which is perhaps clearer and prevents bad types such as (Int -> String &
Int -> Char) by construction.

While it may be impossible (?) to infer such a type for f, would it be
possible to make use of such an annotation (esp since Haskell with GHC
extensions already has arbitary rank polymorphism)?

Also, as a second point, could functional dependencies in type classes be
written using a similar syntax eg instead of

    class Insert t c a | c a -> t where
        insert :: t -> c a -> c a

we could write:

    class Insert (h (c a)) c a where
        insert :: h (c a) -> c a -> c a

or
    class Insert t@(h (c a)) c a where   -- re-using as-pattern syntax
        insert :: t -> c a -> c a

to avoid having to have a special syntax just for functional dependencies
and/or to be able to write more complicated fundeps more succinctly?

Regards,
Brian Hulley

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

RE: Intersection types for Haskell?

José Miguel Vilaça
Hi

If I understand your problem than the following is a solution:

--------------------------------------------------

{-# OPTIONS -fglasgow-exts #-}

class Foo a b where
   g :: a -> b

type A = {- change the following -} Int
type B = {- change the following -} Char
   
instance Foo A B where
   g a = {- change the following -} ' '
   
type C = {- change the following -} Float
type D = {- change the following -} String

instance Foo C D where
   g c = {- change the following -} ""
 
 
f :: (Foo a b, Foo c d) => a -> c -> (b, d)  
f x y = (g x, g y)

---------------------------------------------------------

Simply create a class an give instances for the wanted types.

The code above is also in a file in attachment.


cheers

José Miguel Vilaça
Departamento de Informática - Universidade do Minho
[hidden email]

 
-----Mensagem original-----
De: [hidden email]
[mailto:[hidden email]] Em nome de Brian Hulley
Enviada: terça-feira, 10 de Janeiro de 2006 18:01
Para: Haskell-cafe
Assunto: [Haskell-cafe] Intersection types for Haskell?

Hi -
I'm wondering if there is any possiblility of getting intersection types
into Haskell. For example, at the moment there is no (proper) typing for:

    f g x y = (g x, g y)

Ideally, I'd like to be able to write:

    f:: (a -> b & c -> d) -> a -> c -> (b,d)

or

    f :: (a -> b a) -> c -> d -> (b c, b d)

which is perhaps clearer and prevents bad types such as (Int -> String &
Int -> Char) by construction.

While it may be impossible (?) to infer such a type for f, would it be
possible to make use of such an annotation (esp since Haskell with GHC
extensions already has arbitary rank polymorphism)?

Also, as a second point, could functional dependencies in type classes be
written using a similar syntax eg instead of

    class Insert t c a | c a -> t where
        insert :: t -> c a -> c a

we could write:

    class Insert (h (c a)) c a where
        insert :: h (c a) -> c a -> c a

or
    class Insert t@(h (c a)) c a where   -- re-using as-pattern syntax
        insert :: t -> c a -> c a

to avoid having to have a special syntax just for functional dependencies
and/or to be able to write more complicated fundeps more succinctly?

Regards,
Brian Hulley

_______________________________________________
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

tep.hs (461 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|

Re: Intersection types for Haskell?

Brian Hulley
In reply to this post by Brian Hulley
José Miguel Vilaça wrote:

> Hi
>
> If I understand your problem than the following is a solution:
>
> --------------------------------------------------
>
> {-# OPTIONS -fglasgow-exts #-}
>
> class Foo a b where
>    g :: a -> b
>
> type A = {- change the following -} Int
> type B = {- change the following -} Char
>
> instance Foo A B where
>    g a = {- change the following -} ' '
>
> type C = {- change the following -} Float
> type D = {- change the following -} String
>
> instance Foo C D where
>    g c = {- change the following -} ""
>
>
> f :: (Foo a b, Foo c d) => a -> c -> (b, d)
> f x y = (g x, g y)

Thanks for the workaround. However this does not seem to be quite so general
as intersection types, because it would only allow me to define f for some
specific g ie the g of Foo, rather than for any general function...

Regards,
Brian Hulley

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

Re: Intersection types for Haskell?

Taral
In reply to this post by Brian Hulley
On 1/10/06, Brian Hulley <[hidden email]> wrote:
> Hi -
> I'm wondering if there is any possiblility of getting intersection types
> into Haskell. For example, at the moment there is no (proper) typing for:
>
>     f g x y = (g x, g y)
>
> Ideally, I'd like to be able to write:
>
>     f:: (a -> b & c -> d) -> a -> c -> (b,d)

I have no idea what kind of function would have type (a -> b & c ->
d). Can you give an example?

>     f :: (a -> b a) -> c -> d -> (b c, b d)

f :: (forall a. a -> b a) -> c -> d -> (b c, b d)

--
Taral <[hidden email]>
"Computer science is no more about computers than astronomy is about
telescopes."
    -- Edsger Dijkstra
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Intersection types for Haskell?

Brian Hulley
Taral wrote:

> On 1/10/06, Brian Hulley <[hidden email]> wrote:
>> Hi -
>> I'm wondering if there is any possiblility of getting intersection
>> types into Haskell. For example, at the moment there is no (proper)
>> typing for:
>>
>>     f g x y = (g x, g y)
>>
>> Ideally, I'd like to be able to write:
>>
>>     f:: (a -> b & c -> d) -> a -> c -> (b,d)
>
> I have no idea what kind of function would have type (a -> b & c ->
> d). Can you give an example?

g x = x

because g 3 = 3 so g has type Int -> Int but also g 'a' = 'a' so g has type
Char -> Char hence g has type Int -> Int & Char -> Char

Also, h x = (x,x) ie Int -> (Int,Int) & Char -> (Char,Char)

The reason I can't just use a -> b for g's type is that then I would have no
way to write out the result of f, since it is not (b,b)

>
>>     f :: (a -> b a) -> c -> d -> (b c, b d)
>
> f :: (forall a. a -> b a) -> c -> d -> (b c, b d)

That would be nice but unfortunately is not accepted by GHC because it
cannot unify a->a with a -> b a, for example the following does not compile:

{-# OPTIONS -fglasgow-exts #-}

f :: (forall a. a -> b a) -> c -> d -> (b c, b d)
f g x y = (g x, g y)

g x = x

main = do
                 putStrLn (show (f g 3 'c'))

Regards,
Brian Hulley

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

Re: Intersection types for Haskell?

Brian Hulley
Brian Hulley wrote:
> Taral wrote:
>> I have no idea what kind of function would have type (a -> b & c ->
>> d). Can you give an example?
>
> g x = x
>
> because g 3 = 3 so g has type Int -> Int but also g 'a' = 'a' so g
> has type Char -> Char hence g has type Int -> Int & Char -> Char

Actually I should have said "g's type *matches* (Int->Int & Char->Char)"
since of course g has type a->a.

Regards, Brian.

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

Re: Intersection types for Haskell?

Brian Hulley
In reply to this post by Brian Hulley
Brian Hulley wrote:
> <snip>
> which is perhaps clearer and prevents bad types such as (Int ->
> String & Int -> Char) by construction.

Oops! I forgot that functions with such types can exist via multi-parameter
type classes and overloading - this may be one reason why intersection types
have not yet been added to Haskell.

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

Re: Intersection types for Haskell?

David Menendez
In reply to this post by Brian Hulley
Brian Hulley writes:

> Also, as a second point, could functional dependencies in type
> classes be written using a similar syntax eg instead of
>
>     class Insert t c a | c a -> t where
>         insert :: t -> c a -> c a
>
> we could write:
>
>     class Insert (h (c a)) c a where
>         insert :: h (c a) -> c a -> c a
>
> or
>     class Insert t@(h (c a)) c a where   -- re-using as-pattern syntax
>         insert :: t -> c a -> c a
>
> to avoid having to have a special syntax just for functional
> dependencies and/or to be able to write more complicated fundeps more
> succinctly?

You might be interested in associated types and associated type
synonyms[1]. These are alternatives to functional dependencies which are
less powerful but possibly easier to use. (Of course, no Haskell
compiler supports them.)

For example:

    class Collection c where
        type Elem c
       
        insert :: Elem c -> c -> c
        ...
   
    instance Collection [a] where
        type Elem [a] = a
       
        insert = (:)
        ...

Your example, in the syntax of associated type synonyms, would look
something like this:

    class Insert c a where
        type T c a
        insert :: T c a -> c a -> c a
       
       
[1]: <http://research.microsoft.com/Users/simonpj/papers/assoc-types/>
--
David Menendez <[hidden email]> | "In this house, we obey the laws
<http://www.eyrie.org/~zednenem>      |        of thermodynamics!"
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Intersection types for Haskell?

Brian Hulley
David Menendez wrote:

> Brian Hulley writes:
>
>> Also, as a second point, could functional dependencies in type
>> classes be written using a similar syntax eg instead of
>>
>>     class Insert t c a | c a -> t where
>>         insert :: t -> c a -> c a
>>
>> we could write:
>>
>>     class Insert (h (c a)) c a where
>>         insert :: h (c a) -> c a -> c a
> <snip>
> Your example, in the syntax of associated type synonyms, would look
> something like this:
>
>     class Insert c a where
>         type T c a
>         insert :: T c a -> c a -> c a

Thanks for the link. I suppose h(c a) can't be used on its own because h is
assumed to be a tycon rather than a general type function, but if this
restriction were lifted, the syntax "h a" meaning "some type determined by a
by the type function h" could be used both for intersection typing and
multi-param type classes.

Regards, Brian.

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