Type families in kind signatures with TypeInType

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

Type families in kind signatures with TypeInType

David Menendez-2
Should the code below work in GHC 8.0.1?

    {-# LANGUAGE TypeInType, TypeFamilies #-}

    import Data.Kind (Type)

    type family K t :: Type
    type family T t :: K t -> Type

    data List

    type instance K List = Type
    type instance T List = []


Right now, I get an error like this one:

min.hs:12:24: error:
    • Expected kind ‘K List -> Type’, but ‘[]’ has kind ‘* -> *’
    • In the type ‘[]’
      In the type instance declaration for ‘T’

which is puzzling, since K List -> Type and * -> * should be the same.

Obviously, TypeInType is experimental and incomplete. I’m just wondering if this sort of thing is expected to work, or if I’m doing something not yet supported or never to be supported

In particular, the kind signature for T is forall t -> K t -> Type, which looks like DependentHaskell.

--

_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

RE: Type families in kind signatures with TypeInType

Haskell - Glasgow-haskell-users mailing list

This is an example of https://ghc.haskell.org/trac/ghc/ticket/12088.

 

The “type instance T List” declaration actually depends on the “type instance K List” declaration; the latter must be typechecked before the former.  But this dependency is absolutely unclear.  There’s a long discussion on the thread.  Bottom line: we don’t know a solid automated way to spot this kind of problem, so  I think we are going to ask for programmer assistance.  In this case, we’d put a “separator” after the “type instance K List” decl, to explain that it must be done first:

 

    type instance K List = Type

    ===========

    type instance T List = []

 

Currently you have to write $(return []) to get the separator, but I think we’ll add a special separator.

 

Simon

 

 

From: Glasgow-haskell-users [mailto:[hidden email]] On Behalf Of David Menendez
Sent: 23 September 2016 05:48
To: [hidden email] Mailing List <[hidden email]>
Subject: Type families in kind signatures with TypeInType

 

Should the code below work in GHC 8.0.1?

 

    {-# LANGUAGE TypeInType, TypeFamilies #-}

 

    import Data.Kind (Type)

 

    type family K t :: Type

    type family T t :: K t -> Type

 

    data List

 

    type instance K List = Type

    type instance T List = []

 

 

Right now, I get an error like this one:

 

min.hs:12:24: error:

    • Expected kind ‘K List -> Type’, but ‘[]’ has kind ‘* -> *’

    • In the type ‘[]’

      In the type instance declaration for ‘T’

 

which is puzzling, since K List -> Type and * -> * should be the same.

 

Obviously, TypeInType is experimental and incomplete. I’m just wondering if this sort of thing is expected to work, or if I’m doing something not yet supported or never to be supported

 

In particular, the kind signature for T is forall t -> K t -> Type, which looks like DependentHaskell.

 

--


_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: Type families in kind signatures with TypeInType

David Menendez-2
On Fri, Sep 23, 2016 at 3:19 AM, Simon Peyton Jones <[hidden email]> wrote:

Interesting. Is this case also an example, or is it a non-feature?

class C t where
    type K t :: Type
    type T t :: K t -> Type

    m :: t -> T t a

min.hs:21:17: error:
    • Type constructor ‘K’ cannot be used here
        (it is defined and used in the same recursive group)
    • In the kind ‘K t -> Type’
Failed, modules loaded: none.

GHC accepts this if K t is moved outside of C.
 

The “type instance T List” declaration actually depends on the “type instance K List” declaration; the latter must be typechecked before the former.  But this dependency is absolutely unclear.  There’s a long discussion on the thread.  Bottom line: we don’t know a solid automated way to spot this kind of problem, so  I think we are going to ask for programmer assistance.  In this case, we’d put a “separator” after the “type instance K List” decl, to explain that it must be done first:

 

    type instance K List = Type

    ===========

    type instance T List = []

 

Currently you have to write $(return []) to get the separator, but I think we’ll add a special separator.


Yes, this works. Thanks.

It would be disappointing if this is the best we can do, but I guess other dependent languages don’t need to deal with open type families and everything being potentially mutually recursive.

--

_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

RE: Type families in kind signatures with TypeInType

Haskell - Glasgow-haskell-users mailing list

Interesting. Is this case also an example, or is it a non-feature?

 

class C t where

    type K t :: Type

    type T t :: K t -> Type

 

    m :: t -> T t a

 

 

Ah, that’s quite different!  We should do strongly-connected-component analysis of the associated-type declarations within a single class declaration…. but we don’t currently do that.   No difficulty in principle, I think.

 

You could open a ticket.   (Do include a link to this email thread and to #12088)

 

Simon

 

 

From: [hidden email] [mailto:[hidden email]] On Behalf Of David Menendez
Sent: 23 September 2016 19:51
To: Simon Peyton Jones <[hidden email]>
Cc: [hidden email] Mailing List <[hidden email]>
Subject: Re: Type families in kind signatures with TypeInType

 

On Fri, Sep 23, 2016 at 3:19 AM, Simon Peyton Jones <[hidden email]> wrote:

 

Interesting. Is this case also an example, or is it a non-feature?

 

class C t where

    type K t :: Type

    type T t :: K t -> Type

 

    m :: t -> T t a

 

min.hs:21:17: error:

    • Type constructor ‘K’ cannot be used here

        (it is defined and used in the same recursive group)

    • In the kind ‘K t -> Type’

Failed, modules loaded: none.

 

GHC accepts this if K t is moved outside of C.

 

The “type instance T List” declaration actually depends on the “type instance K List” declaration; the latter must be typechecked before the former.  But this dependency is absolutely unclear.  There’s a long discussion on the thread.  Bottom line: we don’t know a solid automated way to spot this kind of problem, so  I think we are going to ask for programmer assistance.  In this case, we’d put a “separator” after the “type instance K List” decl, to explain that it must be done first:

 

    type instance K List = Type

    ===========

    type instance T List = []

 

Currently you have to write $(return []) to get the separator, but I think we’ll add a special separator.

 

Yes, this works. Thanks.

 

It would be disappointing if this is the best we can do, but I guess other dependent languages don’t need to deal with open type families and everything being potentially mutually recursive.

 

--


_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: Type families in kind signatures with TypeInType

David Menendez-2
On Fri, Sep 23, 2016 at 3:00 PM, Simon Peyton Jones <[hidden email]> wrote:

Interesting. Is this case also an example, or is it a non-feature?

 

class C t where

    type K t :: Type

    type T t :: K t -> Type

 

    m :: t -> T t a

 

 

Ah, that’s quite different!  We should do strongly-connected-component analysis of the associated-type declarations within a single class declaration…. but we don’t currently do that.   No difficulty in principle, I think.

 

You could open a ticket.   (Do include a link to this email thread and to #12088)


I’ve opened ticket #12612 <https://ghc.haskell.org/trac/ghc/ticket/12612>.

Assuming GHC accepted this definition, would the Template Haskell trick (or whatever replaces it) allow defining instances of C?

--

_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users
Loading...