Edward Kmett | 31 Aug 04:38 2012
Picon

PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?

If I define the following

{-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures, MultiParamTypeClasses, PolyKinds, RankNTypes, TypeOperators, DefaultSignatures, DataKinds, FlexibleInstances, UndecidableInstances #-}
module Indexed.Test where

class IMonad (m :: (k -> *) -> k -> *) where 
  ireturn :: a x -> m a x

infixr 5 :-
data Thrist :: ((i,i) -> *) -> (i,i) -> * where
  Nil :: Thrist a '(i,i)
  (:-) :: a '(i,j) -> Thrist a '(j,k) -> Thrist a '(i,k)

instance IMonad Thrist where
  ireturn a = a :- Nil

Then 'ireturn' complains (correctly) that it can't match the k with the kind (i,i). The reason it can't is because when you look at the resulting signature for the MPTC it generates it looks like

class IMonad k m where
  ireturn :: a x -> m a x

However, there doesn't appear to be a way to say that the kind k should be determined by m. 

I tried doing:

class IMonad (m :: (k -> *) -> k -> *) | m -> k where 
  ireturn :: a x -> m a x

Surprisingly (to me) this compiles and generates the correct constraints for IMonad:

ghci> :set -XPolyKinds -XKindSignatures -XFunctionalDependencies -XDataKinds -XGADTs
ghci> class IMonad (m :: (k -> *) -> k -> *) | m -> k where ireturn :: a x -> m a x
ghci> :info IMonad
class IMonad k m | m -> k where
  ireturn :: a x -> m a x

But when I add 

ghci> :{
Prelude| data Thrist :: ((i,i) -> *) -> (i,i) -> * where
Prelude|   Nil :: Thrist a '(i,i)
Prelude|   (:-) :: a '(i,j) -> Thrist a '(j,k) -> Thrist a '(i,k)
Prelude| :}

and attempt to introduce the instance, I crash:

ghci> instance IMonad Thrist where ireturn a = a :- Nil
ghc: panic! (the 'impossible' happened)
  (GHC version 7.6.0.20120810 for x86_64-apple-darwin):
lookupVarEnv_NF: Nothing

Please report this as a GHC bug:  http://www.haskell.org/ghc/reportabug

Moreover, attempting to compile them in separate modules leads to a different issue. 

Within the module, IMonad has a type that includes the kind k and the constraint on it from m. But from the other module, :info shows no such constraint, and the above code again fails to typecheck, but upon trying to recompile, when GHC goes to load the IMonad instance from the core file, it panicks again differently about references to a variable not present in the core.

Is there any way to make such a constraint that determines a kind from a type parameter in GHC 7.6 at this time?

I tried the Kind hack used in GHC.TypeLits, but it doesn't seem to be applicable to this situation.

-Edward
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Richard Eisenberg | 31 Aug 05:04 2012

Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?

This looks related to bug #7128. In the response to that (fixed, closed) bug report, Simon PJ said that functional dependencies involving kinds are supported. Are you compiling with a version of 7.6 updated since that bug fix?

Richard

On Aug 30, 2012, at 10:38 PM, Edward Kmett wrote:

If I define the following

{-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures, MultiParamTypeClasses, PolyKinds, RankNTypes, TypeOperators, DefaultSignatures, DataKinds, FlexibleInstances, UndecidableInst ances #-}
module Indexed.Test where

class IMonad (m :: (k -> *) -> k -> *) where 
  ireturn :: a x -> m a x

infixr 5 :-
data Thrist :: ((i,i) -> *) -> (i,i) -> * where
  Nil :: Thrist a '(i,i)
  (:-) :: a '(i,j) -> Thrist a '(j,k) -> Thrist a '(i,k)

instance IMonad Thrist where
  ireturn a = a :- Nil

Then 'ireturn' complains (correctly) that it can't match the k with the kind (i,i). The reason it can't is because when you look at the resulting signature for the MPTC it generates it looks like

class IMonad k m where
  ireturn :: a x -> m a x

However, there doesn't appear to be a way to say that the kind k should be determined by m. 

I tried doing:

class IMonad (m :: (k -> *) -> k -> *) | m -> k where 
  ireturn :: a x -> m a x

Surprisingly (to me) this compiles and generates the correct constraints for IMonad:

ghci> :set -XPolyKinds -XKindSignatures -XFunctionalDependencies -XDataKinds -XGADTs
ghci> class IMonad (m :: (k -> *) -> k -> *) | m -> k where ireturn :: a x -> m a x
ghci> :info IMonad
class IMonad k m | m -> k where
  ireturn :: a x -> m a x

But when I add 

ghci> :{
Prelude| data Thrist :: ((i,i) -> *) -> (i,i) -> * where
Prelude|   Nil :: Thrist a '(i,i)
Prelude|   (:-) :: a '(i,j) -> Thrist a '(j,k) -> Thrist a '(i,k)
Prelude| :}

and attempt to introduce the instance, I crash:

ghci> instance IMonad Thrist where ireturn a = a :- Nil
ghc: panic! (the 'impossible' happened)
  (GHC version 7.6.0.20120810 for x86_64-apple-darwin):
lookupVarEnv_NF: Nothing

Please report this as a GHC bug:  http://www.haskell.org/ghc/reportabug

Moreover, attempting to compile them in separate modules leads to a different issue. 

Within the module, IMonad has a type that includes the kind k and the constraint on it from m. But from the other module, :info shows no such constraint, and the above code again fails to typecheck, but upon trying to recompile, when GHC goes to load the IMonad instance from the core file, it panicks again differently about references to a variable not present in the core.

Is there any way to make such a constraint that determines a kind from a type parameter in GHC 7.6 at this time?

I tried the Kind hack used in GHC.TypeLits, but it doesn't seem to be applicable to this situation.

-Edward
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Edward Kmett | 31 Aug 14:13 2012
Picon

Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?

I tried this with the release candidate. I can go pull a more recent version and try again.

On Thu, Aug 30, 2012 at 11:04 PM, Richard Eisenberg <eir <at> cis.upenn.edu> wrote:
This looks related to bug #7128. In the response to that (fixed, closed) bug report, Simon PJ said that functional dependencies involving kinds are supported. Are you compiling with a version of 7.6 updated since that bug fix?

Richard

On Aug 30, 2012, at 10:38 PM, Edward Kmett wrote:

If I define the following

{-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures, MultiParamTypeClasses, PolyKinds, RankNTypes, TypeOperators, DefaultSignatures, DataKinds, FlexibleInstances, UndecidableInstances #-}
module Indexed.Test where

class IMonad (m :: (k -> *) -> k -> *) where 
  ireturn :: a x -> m a x

infixr 5 :-
data Thrist :: ((i,i) -> *) -> (i,i) -> * where
  Nil :: Thrist a '(i,i)
  (:-) :: a '(i,j) -> Thrist a '(j,k) -> Thrist a '(i,k)

instance IMonad Thrist where
  ireturn a = a :- Nil

Then 'ireturn' complains (correctly) that it can't match the k with the kind (i,i). The reason it can't is because when you look at the resulting signature for the MPTC it generates it looks like

class IMonad k m where
  ireturn :: a x -> m a x

However, there doesn't appear to be a way to say that the kind k should be determined by m. 

I tried doing:

class IMonad (m :: (k -> *) -> k -> *) | m -> k where 
  ireturn :: a x -> m a x

Surprisingly (to me) this compiles and generates the correct constraints for IMonad:

ghci> :set -XPolyKinds -XKindSignatures -XFunctionalDependencies -XDataKinds -XGADTs
ghci> class IMonad (m :: (k -> *) -> k -> *) | m -> k where ireturn :: a x -> m a x
ghci> :info IMonad
class IMonad k m | m -> k where
  ireturn :: a x -> m a x

But when I add 

ghci> :{
Prelude| data Thrist :: ((i,i) -> *) -> (i,i) -> * where
Prelude|   Nil :: Thrist a '(i,i)
Prelude|   (:-) :: a '(i,j) -> Thrist a '(j,k) -> Thrist a '(i,k)
Prelude| :}

and attempt to introduce the instance, I crash:

ghci> instance IMonad Thrist where ireturn a = a :- Nil
ghc: panic! (the 'impossible' happened)
  (GHC version 7.6.0.20120810 for x86_64-apple-darwin):
lookupVarEnv_NF: Nothing

Please report this as a GHC bug:  http://www.haskell.org/ghc/reportabug

Moreover, attempting to compile them in separate modules leads to a different issue. 

Within the module, IMonad has a type that includes the kind k and the constraint on it from m. But from the other module, :info shows no such constraint, and the above code again fails to typecheck, but upon trying to recompile, when GHC goes to load the IMonad instance from the core file, it panicks again differently about references to a variable not present in the core.

Is there any way to make such a constraint that determines a kind from a type parameter in GHC 7.6 at this time?

I tried the Kind hack used in GHC.TypeLits, but it doesn't seem to be applicable to this situation.

-Edward
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users


_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Simon Peyton-Jones | 31 Aug 11:55 2012
Picon

RE: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?

With the code below, I get this error message with HEAD. And that looks right to me, no?

The current 7.6 branch gives the same message printed less prettily.

 

If I replace the defn of irt with

irt :: a '(i,j) -> Thrist a '(i,j)

irt ax = ax :- Nil

 

then it typechecks.

 

Simon

 

 

Knett.hs:20:10:

    Couldn't match type `x' with '(i0, k0)

      `x' is a rigid type variable bound by

          the type signature for irt :: a x -> Thrist k a x at Knett.hs:19:8

    Expected type: Thrist k a x

      Actual type: Thrist k a '(i0, k0)

    In the expression: ax :- Nil

    In an equation for `irt': irt ax = ax :- Nil

simonpj <at> cam-05-unx:~/tmp$

 

 

{-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures, MultiParamTypeClasses, PolyKinds,

             RankNTypes, TypeOperators, DefaultSignatures, DataKinds,

             FlexibleInstances, UndecidableInstances #-}

 

module Knett where

 

class IMonad (m :: (k -> *) -> k -> *) | m -> k where

  ireturn :: a x -> m a x

 

infixr 5 :-

 

data Thrist :: ((i,i) -> *) -> (i,i) -> * where

  Nil  :: Thrist a '(i,i)

  (:-) :: a '(i,j) -> Thrist a '(j,k) -> Thrist a '(i,k)

 

-- instance IMonad Thrist where

--  ireturn a = a :- Nil

 

irt :: a x -> Thrist a x

irt ax = ax :- Nil

 

 

From: glasgow-haskell-users-bounces <at> haskell.org [mailto:glasgow-haskell-users-bounces <at> haskell.org] On Behalf Of Edward Kmett
Sent: 31 August 2012 03:38
To: glasgow-haskell-users <at> haskell.org
Subject: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?

 

If I define the following

 

{-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures, MultiParamTypeClasses, PolyKinds, RankNTypes, TypeOperators, DefaultSignatures, DataKinds, FlexibleInstances, UndecidableInstances #-}

module Indexed.Test where

 

class IMonad (m :: (k -> *) -> k -> *) where 

  ireturn :: a x -> m a x

 

infixr 5 :-

data Thrist :: ((i,i) -> *) -> (i,i) -> * where

  Nil :: Thrist a '(i,i)

  (:-) :: a '(i,j) -> Thrist a '(j,k) -> Thrist a '(i,k)

 

instance IMonad Thrist where

  ireturn a = a :- Nil

 

Then 'ireturn' complains (correctly) that it can't match the k with the kind (i,i). The reason it can't is because when you look at the resulting signature for the MPTC it generates it looks like

 

class IMonad k m where

  ireturn :: a x -> m a x

 

However, there doesn't appear to be a way to say that the kind k should be determined by m. 

 

I tried doing:

 

class IMonad (m :: (k -> *) -> k -> *) | m -> k where 

  ireturn :: a x -> m a x

 

Surprisingly (to me) this compiles and generates the correct constraints for IMonad:

 

ghci> :set -XPolyKinds -XKindSignatures -XFunctionalDependencies -XDataKinds -XGADTs

ghci> class IMonad (m :: (k -> *) -> k -> *) | m -> k where ireturn :: a x -> m a x

ghci> :info IMonad

class IMonad k m | m -> k where

  ireturn :: a x -> m a x

 

But when I add 

 

ghci> :{

Prelude| data Thrist :: ((i,i) -> *) -> (i,i) -> * where

Prelude|   Nil :: Thrist a '(i,i)

Prelude|   (:-) :: a '(i,j) -> Thrist a '(j,k) -> Thrist a '(i,k)

Prelude| :}

 

and attempt to introduce the instance, I crash:

 

ghci> instance IMonad Thrist where ireturn a = a :- Nil

ghc: panic! (the 'impossible' happened)

  (GHC version 7.6.0.20120810 for x86_64-apple-darwin):

    lookupVarEnv_NF: Nothing

 

Please report this as a GHC bug:  http://www.haskell.org/ghc/reportabug

 

Moreover, attempting to compile them in separate modules leads to a different issue. 

 

Within the module, IMonad has a type that includes the kind k and the constraint on it from m. But from the other module, :info shows no such constraint, and the above code again fails to typecheck, but upon trying to recompile, when GHC goes to load the IMonad instance from the core file, it panicks again differently about references to a variable not present in the core.

 

Is there any way to make such a constraint that determines a kind from a type parameter in GHC 7.6 at this time?

 

I tried the Kind hack used in GHC.TypeLits, but it doesn't seem to be applicable to this situation.

 

-Edward

_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Edward Kmett | 31 Aug 14:44 2012
Picon

Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?

Hrmm. This seems to render product kinds rather useless, as there is no way to refine the code to reflect the knowledge that they are inhabited by a single constructor. =( 


For instance, there doesn't even seem to be a way to make the following code compile, either.


{-# LANGUAGE PolyKinds, DataKinds, TypeOperators, GADTs #-}
module Product where

import Prelude hiding (id,(.))

class Category k where
  id :: k a a
  (.) :: k b c -> k a b -> k a c

data (*) :: (x -> x -> *) -> (y -> y -> *) -> (x,y) -> (x,y) -> * where
  (:*) :: x a b -> y c d -> (x * y) '(a,c) '(b,d)

instance (Category x, Category y) => Category (x * y) where
  id = id :* id
  (xf :*  yf) . (xg :* yg) = (xf . xg) :* (yf . yg)

This all works perfectly fine in Conor's SHE, (as does the thrist example) so I'm wondering where the impedence mismatch comes in and how to gain knowledge of this injectivity to make it work.

Also, does it ever make sense for the kind of a kind variable mentioned in a type not to get a functional dependency on the type? 

e.g. should

class Foo (m :: k -> *)

always be

class Foo (m :: k -> *) | m -> k

?

Honest question. I can't come up with a scenario, but you might have one I don't know.

-Edward

On Fri, Aug 31, 2012 at 5:55 AM, Simon Peyton-Jones <simonpj <at> microsoft.com> wrote:

With the code below, I get this error message with HEAD. And that looks right to me, no?

The current 7.6 branch gives the same message printed less prettily.

 

If I replace the defn of irt with

irt :: a '(i,j) -> Thrist a '(i,j)

irt ax = ax :- Nil

 

then it typechecks.

 

Simon

 

 

Knett.hs:20:10:

    Couldn't match type `x' with '(i0, k0)

      `x' is a rigid type variable bound by

          the type signature for irt :: a x -> Thrist k a x at Knett.hs:19:8

    Expected type: Thrist k a x

      Actual type: Thrist k a '(i0, k0)

    In the expression: ax :- Nil

    In an equation for `irt': irt ax = ax :- Nil

simonpj <at> cam-05-unx:~/tmp$

 

 

{-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures, MultiParamTypeClasses, PolyKinds,

             RankNTypes, TypeOperators, DefaultSignatures, DataKinds,

             FlexibleInstances, UndecidableInstances #-}

 

module Knett where

 

class IMonad (m :: (k -> *) -> k -> *) | m -> k where

  ireturn :: a x -> m a x

 

infixr 5 :-

 

data Thrist :: ((i,i) -> *) -> (i,i) -> * where

  Nil  :: Thrist a '(i,i)

  (:-) :: a '(i,j) -> Thrist a '(j,k) -> Thrist a '(i,k)

 

-- instance IMonad Thrist where

--  ireturn a = a :- Nil

 

irt :: a x -> Thrist a x

irt ax = ax :- Nil

 

 

From: glasgow-haskell-users-bounces <at> haskell.org [mailto:glasgow-haskell-users-bounces <at> haskell.org] On Behalf Of Edward Kmett
Sent: 31 August 2012 03:38
To: glasgow-haskell-users <at> haskell.org
Subject: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?

 

If I define the following

 

{-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures, MultiParamTypeClasses, PolyKinds, RankNTypes, TypeOperators, DefaultSignatures, DataKinds, FlexibleInstances, UndecidableInstances #-}

module Indexed.Test where

 

class IMonad (m :: (k -> *) -> k -> *) where 

  ireturn :: a x -> m a x

 

infixr 5 :-

data Thrist :: ((i,i) -> *) -> (i,i) -> * where

  Nil :: Thrist a '(i,i)

  (:-) :: a '(i,j) -> Thrist a '(j,k) -> Thrist a '(i,k)

 

instance IMonad Thrist where

  ireturn a = a :- Nil

 

Then 'ireturn' complains (correctly) that it can't match the k with the kind (i,i). The reason it can't is because when you look at the resulting signature for the MPTC it generates it looks like

 

class IMonad k m where

  ireturn :: a x -> m a x

 

However, there doesn't appear to be a way to say that the kind k should be determined by m. 

 

I tried doing:

 

class IMonad (m :: (k -> *) -> k -> *) | m -> k where 

  ireturn :: a x -> m a x

 

Surprisingly (to me) this compiles and generates the correct constraints for IMonad:

 

ghci> :set -XPolyKinds -XKindSignatures -XFunctionalDependencies -XDataKinds -XGADTs

ghci> class IMonad (m :: (k -> *) -> k -> *) | m -> k where ireturn :: a x -> m a x

ghci> :info IMonad

class IMonad k m | m -> k where

  ireturn :: a x -> m a x

 

But when I add 

 

ghci> :{

Prelude| data Thrist :: ((i,i) -> *) -> (i,i) -> * where

Prelude|   Nil :: Thrist a '(i,i)

Prelude|   (:-) :: a '(i,j) -> Thrist a '(j,k) -> Thrist a '(i,k)

Prelude| :}

 

and attempt to introduce the instance, I crash:

 

ghci> instance IMonad Thrist where ireturn a = a :- Nil

ghc: panic! (the 'impossible' happened)

  (GHC version 7.6.0.20120810 for x86_64-apple-darwin):

    lookupVarEnv_NF: Nothing

 

Please report this as a GHC bug:  http://www.haskell.org/ghc/reportabug

 

Moreover, attempting to compile them in separate modules leads to a different issue. 

 

Within the module, IMonad has a type that includes the kind k and the constraint on it from m. But from the other module, :info shows no such constraint, and the above code again fails to typecheck, but upon trying to recompile, when GHC goes to load the IMonad instance from the core file, it panicks again differently about references to a variable not present in the core.

 

Is there any way to make such a constraint that determines a kind from a type parameter in GHC 7.6 at this time?

 

I tried the Kind hack used in GHC.TypeLits, but it doesn't seem to be applicable to this situation.

 

-Edward


_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Edward Kmett | 31 Aug 14:55 2012
Picon

Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?

Hrmm. This seems to work manually for getting product categories to work. Perhaps I can do the same thing for thrists.


{-# LANGUAGE PolyKinds, DataKinds, TypeOperators, GADTs, TypeFamilies #-}
module Product where

import Prelude hiding (id,(.))

class Category k where
  id :: k a a
  (.) :: k b c -> k a b -> k a c

type family Fst (a :: (p,q)) :: p
type instance Fst '(p,q) = p

type family Snd (a :: (p,q)) :: q
type instance Snd '(p,q) = q

data (*) :: (x -> x -> *) -> (y -> y -> *) -> (x,y) -> (x,y) -> * where
  (:*) :: x (Fst a) (Fst b) -> y (Snd a) (Snd b) -> (x * y) a b

instance (Category x, Category y) => Category (x * y) where
  id = id :* id
  (xf :*  yf) . (xg :* yg) = (xf . xg) :* (yf . yg)



On Fri, Aug 31, 2012 at 8:44 AM, Edward Kmett <ekmett <at> gmail.com> wrote:
Hrmm. This seems to render product kinds rather useless, as there is no way to refine the code to reflect the knowledge that they are inhabited by a single constructor. =( 

For instance, there doesn't even seem to be a way to make the following code compile, either.


{-# LANGUAGE PolyKinds, DataKinds, TypeOperators, GADTs #-}
module Product where

import Prelude hiding (id,(.))

class Category k where
  id :: k a a
  (.) :: k b c -> k a b -> k a c

data (*) :: (x -> x -> *) -> (y -> y -> *) -> (x,y) -> (x,y) -> * where
  (:*) :: x a b -> y c d -> (x * y) '(a,c) '(b,d)

instance (Category x, Category y) => Category (x * y) where
  id = id :* id
  (xf :*  yf) . (xg :* yg) = (xf . xg) :* (yf . yg)

This all works perfectly fine in Conor's SHE, (as does the thrist example) so I'm wondering where the impedence mismatch comes in and how to gain knowledge of this injectivity to make it work.

Also, does it ever make sense for the kind of a kind variable mentioned in a type not to get a functional dependency on the type? 

e.g. should

class Foo (m :: k -> *)

always be

class Foo (m :: k -> *) | m -> k

?

Honest question. I can't come up with a scenario, but you might have one I don't know.

-Edward

On Fri, Aug 31, 2012 at 5:55 AM, Simon Peyton-Jones <simonpj <at> microsoft.com> wrote:

With the code below, I get this error message with HEAD. And that looks right to me, no?

The current 7.6 branch gives the same message printed less prettily.

 

If I replace the defn of irt with

irt :: a '(i,j) -> Thrist a '(i,j)

irt ax = ax :- Nil

 

then it typechecks.

 

Simon

 

 

Knett.hs:20:10:

    Couldn't match type `x' with '(i0, k0)

      `x' is a rigid type variable bound by

          the type signature for irt :: a x -> Thrist k a x at Knett.hs:19:8

    Expected type: Thrist k a x

      Actual type: Thrist k a '(i0, k0)

    In the expression: ax :- Nil

    In an equation for `irt': irt ax = ax :- Nil

simonpj <at> cam-05-unx:~/tmp$

 

 

{-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures, MultiParamTypeClasses, PolyKinds,

             RankNTypes, TypeOperators, DefaultSignatures, DataKinds,

             FlexibleInstances, UndecidableInstances #-}

 

module Knett where

 

class IMonad (m :: (k -> *) -> k -> *) | m -> k where

  ireturn :: a x -> m a x

 

infixr 5 :-

 

data Thrist :: ((i,i) -> *) -> (i,i) -> * where

  Nil  :: Thrist a '(i,i)

  (:-) :: a '(i,j) -> Thrist a '(j,k) -> Thrist a '(i,k)

 

-- instance IMonad Thrist where

--  ireturn a = a :- Nil

 

irt :: a x -> Thrist a x

irt ax = ax :- Nil

 

 

From: glasgow-haskell-users-bounces <at> haskell.org [mailto:glasgow-haskell-users-bounces <at> haskell.org] On Behalf Of Edward Kmett
Sent: 31 August 2012 03:38
To: glasgow-haskell-users <at> haskell.org
Subject: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?

 

If I define the following

 

{-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures, MultiParamTypeClasses, PolyKinds, RankNTypes, TypeOperators, DefaultSignatures, DataKinds, FlexibleInstances, UndecidableInstances #-}

module Indexed.Test where

 

class IMonad (m :: (k -> *) -> k -> *) where 

  ireturn :: a x -> m a x

 

infixr 5 :-

data Thrist :: ((i,i) -> *) -> (i,i) -> * where

  Nil :: Thrist a '(i,i)

  (:-) :: a '(i,j) -> Thrist a '(j,k) -> Thrist a '(i,k)

 

instance IMonad Thrist where

  ireturn a = a :- Nil

 

Then 'ireturn' complains (correctly) that it can't match the k with the kind (i,i). The reason it can't is because when you look at the resulting signature for the MPTC it generates it looks like

 

class IMonad k m where

  ireturn :: a x -> m a x

 

However, there doesn't appear to be a way to say that the kind k should be determined by m. 

 

I tried doing:

 

class IMonad (m :: (k -> *) -> k -> *) | m -> k where 

  ireturn :: a x -> m a x

 

Surprisingly (to me) this compiles and generates the correct constraints for IMonad:

 

ghci> :set -XPolyKinds -XKindSignatures -XFunctionalDependencies -XDataKinds -XGADTs

ghci> class IMonad (m :: (k -> *) -> k -> *) | m -> k where ireturn :: a x -> m a x

ghci> :info IMonad

class IMonad k m | m -> k where

  ireturn :: a x -> m a x

 

But when I add 

 

ghci> :{

Prelude| data Thrist :: ((i,i) -> *) -> (i,i) -> * where

Prelude|   Nil :: Thrist a '(i,i)

Prelude|   (:-) :: a '(i,j) -> Thrist a '(j,k) -> Thrist a '(i,k)

Prelude| :}

 

and attempt to introduce the instance, I crash:

 

ghci> instance IMonad Thrist where ireturn a = a :- Nil

ghc: panic! (the 'impossible' happened)

  (GHC version 7.6.0.20120810 for x86_64-apple-darwin):

    lookupVarEnv_NF: Nothing

 

Please report this as a GHC bug:  http://www.haskell.org/ghc/reportabug

 

Moreover, attempting to compile them in separate modules leads to a different issue. 

 

Within the module, IMonad has a type that includes the kind k and the constraint on it from m. But from the other module, :info shows no such constraint, and the above code again fails to typecheck, but upon trying to recompile, when GHC goes to load the IMonad instance from the core file, it panicks again differently about references to a variable not present in the core.

 

Is there any way to make such a constraint that determines a kind from a type parameter in GHC 7.6 at this time?

 

I tried the Kind hack used in GHC.TypeLits, but it doesn't seem to be applicable to this situation.

 

-Edward



_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Edward Kmett | 31 Aug 15:06 2012
Picon

Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?

This works, though it'll be all sorts of fun to try to scale up. 


{-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures, MultiParamTypeClasses, PolyKinds, RankNTypes, TypeOperators, DefaultSignatures, DataKinds, FlexibleInstances, UndecidableInstances, TypeFamilies #-}
module Indexed.Test where

class IMonad (m :: (k -> *) -> k -> *) | m -> k
  where ireturn :: a x -> m a x

type family Fst (a :: (p,q)) :: p
type instance Fst '(p,q) = p

type family Snd (a :: (p,q)) :: q
type instance Snd '(p,q) = q

infixr 5 :-
data Thrist :: ((i,i) -> *) -> (i,i) -> * where
  Nil :: Thrist a '(i,i)
  (:-) :: (Snd ij ~ Fst jk, Fst ij ~ Fst ik, Snd jk ~ Snd ik) => a ij -> Thrist a jk -> Thrist a ik

instance IMonad Thrist where 
  ireturn a = a :- Nil

I know Agda has to jump through some hoops to make the refinement work on pairs when they do eta expansion. I wonder if this could be made less painful.


On Fri, Aug 31, 2012 at 8:55 AM, Edward Kmett <ekmett <at> gmail.com> wrote:
Hrmm. This seems to work manually for getting product categories to work. Perhaps I can do the same thing for thrists.

{-# LANGUAGE PolyKinds, DataKinds, TypeOperators, GADTs, TypeFamilies #-}
module Product where

import Prelude hiding (id,(.))

class Category k where
  id :: k a a
  (.) :: k b c -> k a b -> k a c

type family Fst (a :: (p,q)) :: p
type instance Fst '(p,q) = p

type family Snd (a :: (p,q)) :: q
type instance Snd '(p,q) = q

data (*) :: (x -> x -> *) -> (y -> y -> *) -> (x,y) -> (x,y) -> * where
  (:*) :: x (Fst a) (Fst b) -> y (Snd a) (Snd b) -> (x * y) a b

instance (Category x, Category y) => Category (x * y) where
  id = id :* id
  (xf :*  yf) . (xg :* yg) = (xf . xg) :* (yf . yg)



On Fri, Aug 31, 2012 at 8:44 AM, Edward Kmett <ekmett <at> gmail.com> wrote:
Hrmm. This seems to render product kinds rather useless, as there is no way to refine the code to reflect the knowledge that they are inhabited by a single constructor. =( 

For instance, there doesn't even seem to be a way to make the following code compile, either.


{-# LANGUAGE PolyKinds, DataKinds, TypeOperators, GADTs #-}
module Product where

import Prelude hiding (id,(.))

class Category k where
  id :: k a a
  (.) :: k b c -> k a b -> k a c

data (*) :: (x -> x -> *) -> (y -> y -> *) -> (x,y) -> (x,y) -> * where
  (:*) :: x a b -> y c d -> (x * y) '(a,c) '(b,d)

instance (Category x, Category y) => Category (x * y) where
  id = id :* id
  (xf :*  yf) . (xg :* yg) = (xf . xg) :* (yf . yg)

This all works perfectly fine in Conor's SHE, (as does the thrist example) so I'm wondering where the impedence mismatch comes in and how to gain knowledge of this injectivity to make it work.

Also, does it ever make sense for the kind of a kind variable mentioned in a type not to get a functional dependency on the type? 

e.g. should

class Foo (m :: k -> *)

always be

class Foo (m :: k -> *) | m -> k

?

Honest question. I can't come up with a scenario, but you might have one I don't know.

-Edward

On Fri, Aug 31, 2012 at 5:55 AM, Simon Peyton-Jones <simonpj <at> microsoft.com> wrote:

With the code below, I get this error message with HEAD. And that looks right to me, no?

The current 7.6 branch gives the same message printed less prettily.

 

If I replace the defn of irt with

irt :: a '(i,j) -> Thrist a '(i,j)

irt ax = ax :- Nil

 

then it typechecks.

 

Simon

 

 

Knett.hs:20:10:

    Couldn't match type `x' with '(i0, k0)

      `x' is a rigid type variable bound by

          the type signature for irt :: a x -> Thrist k a x at Knett.hs:19:8

    Expected type: Thrist k a x

      Actual type: Thrist k a '(i0, k0)

    In the expression: ax :- Nil

    In an equation for `irt': irt ax = ax :- Nil

simonpj <at> cam-05-unx:~/tmp$

 

 

{-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures, MultiParamTypeClasses, PolyKinds,

             RankNTypes, TypeOperators, DefaultSignatures, DataKinds,

             FlexibleInstances, UndecidableInstances #-}

 

module Knett where

 

class IMonad (m :: (k -> *) -> k -> *) | m -> k where

  ireturn :: a x -> m a x

 

infixr 5 :-

 

data Thrist :: ((i,i) -> *) -> (i,i) -> * where

  Nil  :: Thrist a '(i,i)

  (:-) :: a '(i,j) -> Thrist a '(j,k) -> Thrist a '(i,k)

 

-- instance IMonad Thrist where

--  ireturn a = a :- Nil

 

irt :: a x -> Thrist a x

irt ax = ax :- Nil

 

 

From: glasgow-haskell-users-bounces <at> haskell.org [mailto:glasgow-haskell-users-bounces <at> haskell.org] On Behalf Of Edward Kmett
Sent: 31 August 2012 03:38
To: glasgow-haskell-users <at> haskell.org
Subject: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?

 

If I define the following

 

{-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures, MultiParamTypeClasses, PolyKinds, RankNTypes, TypeOperators, DefaultSignatures, DataKinds, FlexibleInstances, UndecidableInstances #-}

module Indexed.Test where

 

class IMonad (m :: (k -> *) -> k -> *) where 

  ireturn :: a x -> m a x

 

infixr 5 :-

data Thrist :: ((i,i) -> *) -> (i,i) -> * where

  Nil :: Thrist a '(i,i)

  (:-) :: a '(i,j) -> Thrist a '(j,k) -> Thrist a '(i,k)

 

instance IMonad Thrist where

  ireturn a = a :- Nil

 

Then 'ireturn' complains (correctly) that it can't match the k with the kind (i,i). The reason it can't is because when you look at the resulting signature for the MPTC it generates it looks like

 

class IMonad k m where

  ireturn :: a x -> m a x

 

However, there doesn't appear to be a way to say that the kind k should be determined by m. 

 

I tried doing:

 

class IMonad (m :: (k -> *) -> k -> *) | m -> k where 

  ireturn :: a x -> m a x

 

Surprisingly (to me) this compiles and generates the correct constraints for IMonad:

 

ghci> :set -XPolyKinds -XKindSignatures -XFunctionalDependencies -XDataKinds -XGADTs

ghci> class IMonad (m :: (k -> *) -> k -> *) | m -> k where ireturn :: a x -> m a x

ghci> :info IMonad

class IMonad k m | m -> k where

  ireturn :: a x -> m a x

 

But when I add 

 

ghci> :{

Prelude| data Thrist :: ((i,i) -> *) -> (i,i) -> * where

Prelude|   Nil :: Thrist a '(i,i)

Prelude|   (:-) :: a '(i,j) -> Thrist a '(j,k) -> Thrist a '(i,k)

Prelude| :}

 

and attempt to introduce the instance, I crash:

 

ghci> instance IMonad Thrist where ireturn a = a :- Nil

ghc: panic! (the 'impossible' happened)

  (GHC version 7.6.0.20120810 for x86_64-apple-darwin):

    lookupVarEnv_NF: Nothing

 

Please report this as a GHC bug:  http://www.haskell.org/ghc/reportabug

 

Moreover, attempting to compile them in separate modules leads to a different issue. 

 

Within the module, IMonad has a type that includes the kind k and the constraint on it from m. But from the other module, :info shows no such constraint, and the above code again fails to typecheck, but upon trying to recompile, when GHC goes to load the IMonad instance from the core file, it panicks again differently about references to a variable not present in the core.

 

Is there any way to make such a constraint that determines a kind from a type parameter in GHC 7.6 at this time?

 

I tried the Kind hack used in GHC.TypeLits, but it doesn't seem to be applicable to this situation.

 

-Edward




_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Dan Doel | 31 Aug 15:31 2012
Picon

Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?

On Fri, Aug 31, 2012 at 9:06 AM, Edward Kmett <ekmett <at> gmail.com> wrote:
> I know Agda has to jump through some hoops to make the refinement work on
> pairs when they do eta expansion. I wonder if this could be made less
> painful.

To flesh this out slightly, there are two options for defining pairs in Agda:

  data Pair1 (A B : Set) : Set where
    _,_ : A -> B -> Pair1 A B

  record Pair2 (A B : Set) : Set where
    constructor _,_
    field
      fst : A
      snd : B

Now, if we have something similar to Thrist indexed by Pair2, we have
no problems, because:

    A p -> M A p

is equal to:

    A (fst p , snd p) -> M A (fst p , snd p)

Which is what we need for the irt definition to make sense. If we
index by Pair1, this won't happen automatically, but we have an
alternate definition of irt:

    irt : {I J : Set} {A : Pair1 I J -> Set} {p : Pair1 I J} -> A p ->
Thrist A p
    irt {I} {J} {A} {i , j} ap = ap :- Nil

The pattern match {i , j} there refines p to be (i , j) everywhere, so
the definition is justified.

Without one of these two options, these definitions seem like they're
going to be cumbersome. Ed seems to have found a way to do it, by what
looks kind of like hand implementing the record version, but it looks
unpleasant.

On another note, it confuses me that m -> k would be necessary at all
in the IMonad definition. k is automatically determined by being part
of the kind of m, and filling in anything else for k would be a type
error, no? It is the same kind of reasoning that goes on in
determining what 'a' is for 'id :: forall a. a -> a' based on the type
of the first argument.

-- Dan
Richard Eisenberg | 31 Aug 15:37 2012

Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?

I ran into this same issue in my own experimentation: if a type variable x has a kind with only one constructor K, GHC does not supply the equality x ~ K y for some fresh type variable y. Perhaps it should. I too had to use similar workarounds to what you have come up with.

One potential problem is the existence of the Any type, which inhabits every kind. Say x gets unified with Any. Then, we would have Any ~ K y, which is an inconsistent coercion (equating two types with distinct ground head types). However, because the RHS is a promoted datatype, we know that this coercion can never be applied to a term. Because equality is homogeneous (i.e. ~ can relate only two types of the same kind), I'm not convinced the existence of Any ~ K y is so bad. (Even with heterogeneous equality, it might work out, given that there is more than one type constructor that results in *...)

Regarding the m -> k fundep: my experiments suggest that this dependency is implied when you have (m :: k), but I guess not when you have k appear in the kind of m in a more complicated way. Currently, there are no kind-level functions, so it appears that m -> k could be implied whenever k appears anywhere in the kind of m. If (when!) there are kind-level functions, we'll have to be more careful.

Richard

On Aug 31, 2012, at 9:06 AM, Edward Kmett wrote:

This works, though it'll be all sorts of fun to try to scale up. 


{-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures, MultiParamTypeClasses, PolyKinds, RankNTypes, TypeOperators, DefaultSignatures, DataKinds, FlexibleInstances, UndecidableInstances, TypeFamilies #-}
module Indexed.Test where

class IMonad (m :: (k -> *) -> k -> *) | m -> k
  where ireturn :: a x -> m a x

type family Fst (a :: (p,q)) :: p
type instance Fst '(p,q) = p

type family Snd (a :: (p,q)) :: q
type instance Snd '(p,q) = q

infixr 5 :-
data Thrist :: ((i,i) -> *) -> (i,i) -> * where
  Nil :: Thrist a '(i,i)
  (:-) :: (Snd ij ~ Fst jk, Fst ij ~ Fst ik, Snd jk ~ Snd ik) => a ij -> Thrist a jk -> Thrist a ik

instance IMonad Thrist where 
  ireturn a = a :- Nil

I know Agda has to jump through some hoops to make the refinement work on pairs when they do eta expansion. I wonder if this could be made less painful.


On Fri, Aug 31, 2012 at 8:55 AM, Edward Kmett <ekmett <at> gmail.com> wrote:
Hrmm. This seems to work manually for getting product categories to work. Perhaps I can do the same thing for thrists.

{-# LANGUAGE PolyKinds, DataKinds, TypeOperators, GADTs, TypeFamilies #-}
module Product where

import Prelude hiding (id,(.))

class Category k where
  id :: k a a
  (.) :: k b c -> k a b -> k a c

type family Fst (a :: (p,q)) :: p
type instance Fst '(p,q) = p

type family Snd (a :: (p,q)) :: q
type instance Snd '(p,q) = q

data (*) :: (x -> x -> *) -> (y -> y -> *) -> (x,y) -> (x,y) -> * where
  (:*) :: x (Fst a) (Fst b) -> y (Snd a) (Snd b) -> (x * y) a b

instance (Category x, Category y) => Category (x * y) where
  id = id :* id
  (xf :*  yf) . (xg :* yg) = (xf . xg) :* (yf . yg)



On Fri, Aug 31, 2012 at 8:44 AM, Edward Kmett <ekmett <at> gmail.com> wrote:
Hrmm. This seems to render product kinds rather useless, as there is no way to refine the code to reflect the knowledge that they are inhabited by a single constructor. =( 

For instance, there doesn't even seem to be a way to make the following code compile, either.


{-# LANGUAGE PolyKinds, DataKinds, TypeOperators, GADTs #-}
module Product where

import Prelude hiding (id,(.))

class Category k where
  id :: k a a
  (.) :: k b c -> k a b -> k a c

data (*) :: (x -> x -> *) -> (y -> y -> *) -> (x,y) -> (x,y) -> * where
  (:*) :: x a b -> y c d -> (x * y) '(a,c) '(b,d)

instance (Category x, Category y) => Category (x * y) where
  id = id :* id
  (xf :*  yf) . (xg :* yg) = (xf . xg) :* (yf . yg)

This all works perfectly fine in Conor's SHE, (as does the thrist example) so I'm wondering where the impedence mismatch comes in and how to gain knowledge of this injectivity to make it work.

Also, does it ever make sense for the kind of a kind variable mentioned in a type not to get a functional dependency on the type? 

e.g. should

class Foo (m :: k -> *)

always be

class Foo (m :: k -> *) | m -> k

?

Honest question. I can't come up with a scenario, but you might have one I don't know.

-Edward

On Fri, Aug 31, 2012 at 5:55 AM, Simon Peyton-Jones <simonpj <at> microsoft.com> wrote:

With the code below, I get this error message with HEAD. And that looks right to me, no?

The current 7.6 branch gives the same message printed less prettily.

 

If I replace the defn of irt with

irt :: a '(i,j) -> Thrist a '(i,j)

irt ax = ax :- Nil

 

then it typechecks.

 

Simon

 

 

Knett.hs:20:10:

    Couldn't match type `x' with '(i0, k0)

      `x' is a rigid type variable bound by

          the type signature for irt :: a x -> Thrist k a x at Knett.hs:19:8

    Expected type: Thrist k a x

      Actual type: Thrist k a '(i0, k0)

    In the expression: ax :- Nil

    In an equation for `irt': irt ax = ax :- Nil

simonpj <at> cam-05-unx:~/tmp$

 

 

{-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures, MultiParamTypeClasses, PolyKinds,

             RankNTypes, TypeOperators, DefaultSignatures, DataKinds,

             FlexibleInstances, UndecidableInstances #-}

 

module Knett where

 

class IMonad (m :: (k -> *) -> k -> *) | m -> k where

  ireturn :: a x -> m a x

 

infixr 5 :-

 

data Thrist :: ((i,i) -> *) -> (i,i) -> * where

  Nil  :: Thrist a '(i,i)

  (:-) :: a '(i,j) -> Thrist a '(j,k) -> Thrist a '(i,k)

 

-- instance IMonad Thrist where

--  ireturn a = a :- Nil

 

irt :: a x -> Thrist a x

irt ax = ax :- Nil

 

 

From: glasgow-haskell-users-bounces <at> haskell.org [mailto:glasgow-haskell-users-bounces <at> haskell.org] On Behalf Of Edward Kmett
Sent: 31 August 2012 03:38
To: glasgow-haskell-users <at> haskell.org
Subject: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?

 

If I define the following

 

{-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures, MultiParamTypeClasses, PolyKinds, RankNTypes, TypeOperators, DefaultSignatures, DataKinds, FlexibleInstances, UndecidableInstances #-}

module Indexed.Test where

 

class IMonad (m :: (k -> *) -> k -> *) where 

  ireturn :: a x -> m a x

 

infixr 5 :-

data Thrist :: ((i,i) -> *) -> (i,i) -> * where

  Nil :: Thrist a '(i,i)

  (:-) :: a '(i,j) -> Thrist a '(j,k) -> Thrist a '(i,k)

 

instance IMonad Thrist where

  ireturn a = a :- Nil

 

Then 'ireturn' complains (correctly) that it can't match the k with the kind (i,i). The reason it can't is because when you look at the resulting signature for the MPTC it generates it looks like

 

class IMonad k m where

  ireturn :: a x -> m a x

 

However, there doesn't appear to be a way to say that the kind k should be determined by m. 

 

I tried doing:

 

class IMonad (m :: (k -> *) -> k -> *) | m -> k where 

  ireturn :: a x -> m a x

 

Surprisingly (to me) this compiles and generates the correct constraints for IMonad:

 

ghci> :set -XPolyKinds -XKindSignatures -XFunctionalDependencies -XDataKinds -XGADTs

ghci> class IMonad (m :: (k -> *) -> k -> *) | m -> k where ireturn :: a x -> m a x

ghci> :info IMonad

class IMonad k m | m -> k where

  ireturn :: a x -> m a x

 

But when I add 

 

ghci> :{

Prelude| data Thrist :: ((i,i) -> *) -> (i,i) -> * where

Prelude|   Nil :: Thrist a '(i,i)

Prelude|   (:-) :: a '(i,j) -> Thrist a '(j,k) -> Thrist a '(i,k)

Prelude| :}

 

and attempt to introduce the instance, I crash:

 

ghci> instance IMonad Thrist where ireturn a = a :- Nil

ghc: panic! (the 'impossible' happened)

  (GHC version 7.6.0.20120810 for x86_64-apple-darwin):

    lookupVarEnv_NF: Nothing

 

Please report this as a GHC bug:  http://www.haskell.org/ghc/reportabug

 

Moreover, attempting to compile them in separate modules leads to a different issue. 

 

Within the module, IMonad has a type that includes the kind k and the constraint on it from m. But from the other module, :info shows no such constraint, and the above code again fails to typecheck, but upon trying to recompile, when GHC goes to load the IMonad instance from the core file, it panicks again differently about references to a variable not present in the core.

 

Is there any way to make such a constraint that determines a kind from a type parameter in GHC 7.6 at this time?

 

I tried the Kind hack used in GHC.TypeLits, but it doesn't seem to be applicable to this situation.

 

-Edward




_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Edward Kmett | 31 Aug 18:12 2012
Picon

Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?

On Fri, Aug 31, 2012 at 9:37 AM, Richard Eisenberg <eir <at> cis.upenn.edu> wrote:
I ran into this same issue in my own experimentation: if a type variable x has a kind with only one constructor K, GHC does not supply the equality x ~ K y for some fresh type variable y. Perhaps it should. I too had to use similar workarounds to what you have come up with.

One potential problem is the existence of the Any type, which inhabits every kind. Say x gets unified with Any. Then, we would have Any ~ K y, which is an inconsistent coercion (equating two types with distinct ground head types). However, because the RHS is a promoted datatype, we know that this coercion can never be applied to a term. Because equality is homogeneous (i.e. ~ can relate only two types of the same kind), I'm not convinced the existence of Any ~ K y is so bad. (Even with heterogeneous equality, it might work out, given that there is more than one type constructor that results in *...)

I think it may have to.

Working the example further runs into a similar problem.

When you go to implement indexed bind, there isn't a way to convince GHC that 

(Snd ij ~ i, Fst ij ~ j) entails (ij ~ '(i,j))

I'm working around it (for now) with unsafeCoerce. :-( 

But it with an explicitly introduced equality this code would just work, like it does in other platforms.

  
Regarding the m -> k fundep: my experiments suggest that this dependency is implied when you have (m :: k), but I guess not when you have k appear in the kind of m in a more complicated way. Currently, there are no kind-level functions, so it appears that m -> k could be implied whenever k appears anywhere in the kind of m. If (when!) there are kind-level functions, we'll have to be more careful.

-Edward
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Simon Peyton-Jones | 31 Aug 18:59 2012
Picon

RE: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?

Hrmm. This seems to render product kinds rather useless, as there is no way to refine the code to reflect the knowledge that they are inhabited by a single constructor. =( 

 

Wait. When you say “This seems to render produce kinds useless”, are you saying that in the code I wrote, you think irt should compile??  I reproduce it below for completeness.

 

Simon

 

{-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures, MultiParamTypeClasses, PolyKinds,

             RankNTypes, TypeOperators, DefaultSignatures, DataKinds,

             FlexibleInstances, UndecidableInstances #-}

 

module Knett where

 

data Thrist :: ((i,i) -> *) -> (i,i) -> * where

  Nil  :: Thrist a '(i,i)

  (:-) :: a '(i,j) -> Thrist a '(j,k) -> Thrist a '(i,k)

 

irt :: a x -> Thrist a x

irt ax = ax :- Nil

 

 

_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Simon Peyton-Jones | 31 Aug 19:00 2012
Picon

RE: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?

Same question.  Do you expect the code below to type-check?  I have stripped it down to essentials.  Currently it’s rejected with

 

    Couldn't match type `a' with '(,) k k1 b0 d0

 

And that seems reasonable, doesn’t it?  After all, in the defn of bidStar, (:*) returns a value of type

     Star x y ‘(a,c) ‘(b,d)

which is manifestly incompatible with the claimed, more polymorphic type.  And this is precisely the same error as comes from your class/instance example below, and for precisely the same reason. 

 

I must be confused.

 

Simon

 

                                                                                                                                       

{-# LANGUAGE PolyKinds, DataKinds, TypeOperators, GADTs #-}

module Product where

 

data Star :: (x -> x -> *) -> (y -> y -> *) -> (x,y) -> (x,y) -> * where

  (:*) :: x a b -> y c d -> Star x y '(a,c) '(b,d)

 

bidStar :: Star T T a a

bidStar = bidT :* bidT

 

data T a b = MkT

 

bidT :: T a a

bidT = MkT

 

 

 

From: Edward Kmett [mailto:ekmett <at> gmail.com]
Sent: 31 August 2012 13:45
To: Simon Peyton-Jones
Cc: glasgow-haskell-users <at> haskell.org
Subject: Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?

 

Hrmm. This seems to render product kinds rather useless, as there is no way to refine the code to reflect the knowledge that they are inhabited by a single constructor. =( 

 

For instance, there doesn't even seem to be a way to make the following code compile, either.

 

 

{-# LANGUAGE PolyKinds, DataKinds, TypeOperators, GADTs #-}

module Product where

 

import Prelude hiding (id,(.))

 

class Category k where

  id :: k a a

  (.) :: k b c -> k a b -> k a c

 

data (*) :: (x -> x -> *) -> (y -> y -> *) -> (x,y) -> (x,y) -> * where

  (:*) :: x a b -> y c d -> (x * y) '(a,c) '(b,d)

 

instance (Category x, Category y) => Category (x * y) where

  id = id :* id

  (xf :*  yf) . (xg :* yg) = (xf . xg) :* (yf . yg)

 

This all works perfectly fine in Conor's SHE, (as does the thrist example) so I'm wondering where the impedence mismatch comes in and how to gain knowledge of this injectivity to make it work.

_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Edward Kmett | 31 Aug 19:26 2012
Picon

Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?

It is both perfectly reasonable and unfortunately useless. :(


The problem is that the "more polymorphic" type isn't any more polymorphic, since (ideally) the product kind (a,b) is only inhabited by things of the form '(x,y).

The product kind has a single constructor. But there is no way to express this at present that is safe.

As it stands, I can fake this to an extent in one direction, by writing

{-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures, MultiParamTypeClasses, PolyKinds, TypeFamilies,
             RankNTypes, TypeOperators, DefaultSignatures, DataKinds,
             FlexibleInstances, UndecidableInstances #-}

module Kmett where

type family Fst (p :: (a,b)) :: a
type instance Fst '(a,b) = a

type family Snd (p :: (a,b)) :: b
type instance Snd '(a,b) = b

data Thrist :: ((i,i) -> *) -> (i,i) -> * where
  Nil  :: Thrist a '(i,i)
  (:-) :: (Fst ij ~ i, Snd ij ~ j, Fst ik ~ i, Snd ik ~ k) =>
          a ij -> Thrist a '(j,k) -> Thrist a ik

irt :: a x -> Thrist a x
irt ax = ax :- Nil

and this compiles, but it just pushes the problem down the road, because with that I can show that given ij :: (x,y), I can build up a tuple '(Fst ij, Snd ij) :: (x,y)

But it doesn't give me that '(Fst ij, Snd ij) ~ ij, which you need later when you go to define an indexed bind, and type families are insufficient to the task. Right now to get this property I'm forced to fake it with unsafeCoerce.

-Edward

On Fri, Aug 31, 2012 at 1:00 PM, Simon Peyton-Jones <simonpj <at> microsoft.com> wrote:

Same question.  Do you expect the code below to type-check?  I have stripped it down to essentials.  Currently it’s rejected with

 

    Couldn't match type `a' with '(,) k k1 b0 d0

 

And that seems reasonable, doesn’t it?  After all, in the defn of bidStar, (:*) returns a value of type

     Star x y ‘(a,c) ‘(b,d)

which is manifestly incompatible with the claimed, more polymorphic type.  And this is precisely the same error as comes from your class/instance example below, and for precisely the same reason. 

 

I must be confused.

 

Simon

 

                                                                                                                                       

{-# LANGUAGE PolyKinds, DataKinds, TypeOperators, GADTs #-}

module Product where

 

data Star :: (x -> x -> *) -> (y -> y -> *) -> (x,y) -> (x,y) -> * where

  (:*) :: x a b -> y c d -> Star x y '(a,c) '(b,d)

 

bidStar :: Star T T a a

bidStar = bidT :* bidT

 

data T a b = MkT

 

bidT :: T a a

bidT = MkT

 

 

 

From: Edward Kmett [mailto:ekmett <at> gmail.com]

Sent: 31 August 2012 13:45
To: Simon Peyton-Jones
Cc: glasgow-haskell-users <at> haskell.org
Subject: Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?

 

Hrmm. This seems to render product kinds rather useless, as there is no way to refine the code to reflect the knowledge that they are inhabited by a single constructor. =( 

 

For instance, there doesn't even seem to be a way to make the following code compile, either.

 

 

{-# LANGUAGE PolyKinds, DataKinds, TypeOperators, GADTs #-}

module Product where

 

import Prelude hiding (id,(.))

 

class Category k where

  id :: k a a

  (.) :: k b c -> k a b -> k a c

 

data (*) :: (x -> x -> *) -> (y -> y -> *) -> (x,y) -> (x,y) -> * where

  (:*) :: x a b -> y c d -> (x * y) '(a,c) '(b,d)

 

instance (Category x, Category y) => Category (x * y) where

  id = id :* id

  (xf :*  yf) . (xg :* yg) = (xf . xg) :* (yf . yg)

 

This all works perfectly fine in Conor's SHE, (as does the thrist example) so I'm wondering where the impedence mismatch comes in and how to gain knowledge of this injectivity to make it work.


_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Edward Kmett | 31 Aug 19:29 2012
Picon

Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?

Also, even after upgrading to HEAD, I'm getting a number of errors like:


[2 of 8] Compiling Indexed.Functor  ( src/Indexed/Functor.hs, dist/build/Indexed/Functor.o )
ghc: panic! (the 'impossible' happened)
  (GHC version 7.7.20120830 for x86_64-apple-darwin):
tc_fd_tyvar
    k{tv aZ8}
    k{tv l} [sig]
    ghc-prim:GHC.Prim.BOX{(w) tc 347}

I'll try to distill this down to a reasonable test case.

-Edward

On Fri, Aug 31, 2012 at 1:26 PM, Edward Kmett <ekmett <at> gmail.com> wrote:
It is both perfectly reasonable and unfortunately useless. :(

The problem is that the "more polymorphic" type isn't any more polymorphic, since (ideally) the product kind (a,b) is only inhabited by things of the form '(x,y).

The product kind has a single constructor. But there is no way to express this at present that is safe.

As it stands, I can fake this to an extent in one direction, by writing

{-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures, MultiParamTypeClasses, PolyKinds, TypeFamilies,
             RankNTypes, TypeOperators, DefaultSignatures, DataKinds,
             FlexibleInstances, UndecidableInstances #-}

module Kmett where

type family Fst (p :: (a,b)) :: a
type instance Fst '(a,b) = a

type family Snd (p :: (a,b)) :: b
type instance Snd '(a,b) = b

data Thrist :: ((i,i) -> *) -> (i,i) -> * where
  Nil  :: Thrist a '(i,i)
  (:-) :: (Fst ij ~ i, Snd ij ~ j, Fst ik ~ i, Snd ik ~ k) =>
          a ij -> Thrist a '(j,k) -> Thrist a ik

irt :: a x -> Thrist a x
irt ax = ax :- Nil

and this compiles, but it just pushes the problem down the road, because with that I can show that given ij :: (x,y), I can build up a tuple '(Fst ij, Snd ij) :: (x,y)

But it doesn't give me that '(Fst ij, Snd ij) ~ ij, which you need later when you go to define an indexed bind, and type families are insufficient to the task. Right now to get this property I'm forced to fake it with unsafeCoerce.

-Edward

On Fri, Aug 31, 2012 at 1:00 PM, Simon Peyton-Jones <simonpj <at> microsoft.com> wrote:

Same question.  Do you expect the code below to type-check?  I have stripped it down to essentials.  Currently it’s rejected with

 

    Couldn't match type `a' with '(,) k k1 b0 d0

 

And that seems reasonable, doesn’t it?  After all, in the defn of bidStar, (:*) returns a value of type

     Star x y ‘(a,c) ‘(b,d)

which is manifestly incompatible with the claimed, more polymorphic type.  And this is precisely the same error as comes from your class/instance example below, and for precisely the same reason. 

 

I must be confused.

 

Simon

 

                                                                                                                                       

{-# LANGUAGE PolyKinds, DataKinds, TypeOperators, GADTs #-}

module Product where

 

data Star :: (x -> x -> *) -> (y -> y -> *) -> (x,y) -> (x,y) -> * where

  (:*) :: x a b -> y c d -> Star x y '(a,c) '(b,d)

 

bidStar :: Star T T a a

bidStar = bidT :* bidT

 

data T a b = MkT

 

bidT :: T a a

bidT = MkT

 

 

 

From: Edward Kmett [mailto:ekmett <at> gmail.com]

Sent: 31 August 2012 13:45
To: Simon Peyton-Jones
Cc: glasgow-haskell-users <at> haskell.org
Subject: Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?

 

Hrmm. This seems to render product kinds rather useless, as there is no way to refine the code to reflect the knowledge that they are inhabited by a single constructor. =( 

 

For instance, there doesn't even seem to be a way to make the following code compile, either.

 

 

{-# LANGUAGE PolyKinds, DataKinds, TypeOperators, GADTs #-}

module Product where

 

import Prelude hiding (id,(.))

 

class Category k where

  id :: k a a

  (.) :: k b c -> k a b -> k a c

 

data (*) :: (x -> x -> *) -> (y -> y -> *) -> (x,y) -> (x,y) -> * where

  (:*) :: x a b -> y c d -> (x * y) '(a,c) '(b,d)

 

instance (Category x, Category y) => Category (x * y) where

  id = id :* id

  (xf :*  yf) . (xg :* yg) = (xf . xg) :* (yf . yg)

 

This all works perfectly fine in Conor's SHE, (as does the thrist example) so I'm wondering where the impedence mismatch comes in and how to gain knowledge of this injectivity to make it work.



_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Simon Peyton-Jones | 31 Aug 21:14 2012
Picon

RE: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?

Try translating into System FC!  It’s not just a question of what the type checker will pass; we also have to produce a well-typed FC program.

 

Remember that (putting in all the kind abstractions and applications:

  Thrist :: forall i.  ((i,i) -> *) -> (i,i) -> *

  (:*) :: forall i j k. forall (a: (i,j) -> *).

            a '(i,j) -> Thrist (j,k) a '(j,k) -> Thrist (i,k) a '(i,k)

 

So consider ‘irt’:

 

irt :: forall i. forall (a : (i,i) -> *). forall (x : (i,i)).

        a x -> Thrist i a x        

irt = /\i. /\(a : (i,i) -> *). /\(x: (i,i). \(ax: a x).

       (:*) ? ? ? ? ax (Nil ...)

 

So, what are the three kind args, and the type arg, to (:*)? 

 

It doesn’t seem to make sense... in the body of irt, (:*) produces a result of type

  Thrist (i,k) a ‘(i,k)

but irt’s signature claims to produce a result of type

  Thrist i a x

So irt’s signature is more polymorphic than its body. 

 

If we give irt a less polymorphic type signature, all is well

 

irt :: forall p,q. forall (a : ((p,q),(p,q)) -> *). forall (x : ((p,q),(p,q))).

        a x -> Thrist (p,q) a x        

 

 

Maybe you can explain what you want in System FC? Type inference and the surface language come after that.  If it can’t be expressed in FC it’s out of court.  Of course we can always beef up System FC.

 

I’m copying Stephanie and Conor who may have light to shed.

 

Simon

 

From: Edward Kmett [mailto:ekmett <at> gmail.com]
Sent: 31 August 2012 18:27
To: Simon Peyton-Jones
Cc: glasgow-haskell-users <at> haskell.org
Subject: Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?

 

It is both perfectly reasonable and unfortunately useless. :(

 

The problem is that the "more polymorphic" type isn't any more polymorphic, since (ideally) the product kind (a,b) is only inhabited by things of the form '(x,y).

 

The product kind has a single constructor. But there is no way to express this at present that is safe.

 

As it stands, I can fake this to an extent in one direction, by writing

 

{-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures, MultiParamTypeClasses, PolyKinds, TypeFamilies,

             RankNTypes, TypeOperators, DefaultSignatures, DataKinds,

             FlexibleInstances, UndecidableInstances #-}

 

module Kmett where

 

type family Fst (p :: (a,b)) :: a

type instance Fst '(a,b) = a

 

type family Snd (p :: (a,b)) :: b

type instance Snd '(a,b) = b

 

data Thrist :: ((i,i) -> *) -> (i,i) -> * where

  Nil  :: Thrist a '(i,i)

  (:-) :: (Fst ij ~ i, Snd ij ~ j, Fst ik ~ i, Snd ik ~ k) =>

          a ij -> Thrist a '(j,k) -> Thrist a ik

 

irt :: a x -> Thrist a x

irt ax = ax :- Nil

 

and this compiles, but it just pushes the problem down the road, because with that I can show that given ij :: (x,y), I can build up a tuple '(Fst ij, Snd ij) :: (x,y)

 

But it doesn't give me that '(Fst ij, Snd ij) ~ ij, which you need later when you go to define an indexed bind, and type families are insufficient to the task. Right now to get this property I'm forced to fake it with unsafeCoerce.

 

-Edward

_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Edward Kmett | 31 Aug 21:24 2012
Picon

Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?

I'm going to defer to Conor on this one, as it is one of the examples from his Kleisli Arrows of Outrageous fortune that I'm translating here. ;)


-Edward

On Fri, Aug 31, 2012 at 3:14 PM, Simon Peyton-Jones <simonpj <at> microsoft.com> wrote:

Try translating into System FC!  It’s not just a question of what the type checker will pass; we also have to produce a well-typed FC program.

 

Remember that (putting in all the kind abstractions and applications:

  Thrist :: forall i.  ((i,i) -> *) -> (i,i) -> *

  (:*) :: forall i j k. forall (a: (i,j) -> *).

            a '(i,j) -> Thrist (j,k) a '(j,k) -> Thrist (i,k) a '(i,k)

 

So consider ‘irt’:

 

irt :: forall i. forall (a : (i,i) -> *). forall (x : (i,i)).

        a x -> Thrist i a x        

irt = /\i. /\(a : (i,i) -> *). /\(x: (i,i). \(ax: a x).

       (:*) ? ? ? ? ax (Nil ...)

 

So, what are the three kind args, and the type arg, to (:*)? 

 

It doesn’t seem to make sense... in the body of irt, (:*) produces a result of type

  Thrist (i,k) a ‘(i,k)

but irt’s signature claims to produce a result of type

  Thrist i a x

So irt’s signature is more polymorphic than its body. 

 

If we give irt a less polymorphic type signature, all is well

 

irt :: forall p,q. forall (a : ((p,q),(p,q)) -> *). forall (x : ((p,q),(p,q))).

        a x -> Thrist (p,q) a x        

 

 

Maybe you can explain what you want in System FC? Type inference and the surface language come after that.  If it can’t be expressed in FC it’s out of court.  Of course we can always beef up System FC.

 

I’m copying Stephanie and Conor who may have light to shed.

 

Simon

 

From: Edward Kmett [mailto:ekmett <at> gmail.com]
Sent: 31 August 2012 18:27


To: Simon Peyton-Jones
Cc: glasgow-haskell-users <at> haskell.org
Subject: Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?

 

It is both perfectly reasonable and unfortunately useless. :(

 

The problem is that the "more polymorphic" type isn't any more polymorphic, since (ideally) the product kind (a,b) is only inhabited by things of the form '(x,y).

 

The product kind has a single constructor. But there is no way to express this at present that is safe.

 

As it stands, I can fake this to an extent in one direction, by writing

 

{-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures, MultiParamTypeClasses, PolyKinds, TypeFamilies,

             RankNTypes, TypeOperators, DefaultSignatures, DataKinds,

             FlexibleInstances, UndecidableInstances #-}

 

module Kmett where

 

type family Fst (p :: (a,b)) :: a

type instance Fst '(a,b) = a

 

type family Snd (p :: (a,b)) :: b

type instance Snd '(a,b) = b

 

data Thrist :: ((i,i) -> *) -> (i,i) -> * where

  Nil  :: Thrist a '(i,i)

  (:-) :: (Fst ij ~ i, Snd ij ~ j, Fst ik ~ i, Snd ik ~ k) =>

          a ij -> Thrist a '(j,k) -> Thrist a ik

 

irt :: a x -> Thrist a x

irt ax = ax :- Nil

 

and this compiles, but it just pushes the problem down the road, because with that I can show that given ij :: (x,y), I can build up a tuple '(Fst ij, Snd ij) :: (x,y)

 

But it doesn't give me that '(Fst ij, Snd ij) ~ ij, which you need later when you go to define an indexed bind, and type families are insufficient to the task. Right now to get this property I'm forced to fake it with unsafeCoerce.

 

-Edward


_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Adam Gundry | 1 Sep 10:25 2012
Picon
Picon

Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?

I'm not Conor, but I'll have a go...

On 31/08/12 20:14, Simon Peyton-Jones wrote:
> Try translating into System FC!  It’s not just a question of what the
> type checker will pass; we also have to produce a well-typed FC program.

As Edward and others have recognised, the problem here is that FC
coercions are not expressive enough to prove eta rules, that is

forall x : (a, b) . x ~ (Fst x, Snd x)

or more generally, that every element of a single-constructor (record)
type is equal to the constructor applied to the projections.

It seems like it should be perfectly fine to assert such a thing as an
axiom, though: FC doesn't care what your equality proof is, provided
it's consistent. Consistency of eta-laws follows from the fact that any
inhabitant of the kind must be built with the sole constructor, unless
you have Any (as Richard observed), in which case all bets are off. Why
did you want Any again?

> So consider ‘irt’:
>
> irt :: forall i. forall (a : (i,i) -> *). forall (x : (i,i)).
> 
>         a x -> Thrist i a x        
> 
> irt = /\i. /\(a : (i,i) -> *). /\(x: (i,i). \(ax: a x).
> 
>        (:*) ? ? ? ? ax (Nil ...)
>  
> So, what are the three kind args, and the type arg, to (:*)? 

Here's my solution:

irt = /\i. /\(a : (i,i) -> *). /\(x: (i,i). \(ax: a x).

        (:*) i i i a (ax |> g1) (Nil i a) |> g2

where

  g1 : a x ~ a '(Fst x, Snd x)
  g1 = < a > (eta x)

  g2 : Thrist i a '(Fst x, Snd x) ~ Thrist i a x
  g2 = < Thrist i a > (sym (eta x))

are coercions derived from the eta axiom above.

Hope this helps, now I should really go on holiday,

Adam

> *From:*Edward Kmett [mailto:ekmett <at> gmail.com]
> *Sent:* 31 August 2012 18:27
> *To:* Simon Peyton-Jones
> *Cc:* glasgow-haskell-users <at> haskell.org
> <mailto:glasgow-haskell-users <at> haskell.org>
> *Subject:* Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a
> functional dependency?
> 
>  
> 
> It is both perfectly reasonable and unfortunately useless. :(
> 
>  
> 
> The problem is that the "more polymorphic" type isn't any more
> polymorphic, since (ideally) the product kind (a,b) is only inhabited by
> things of the form '(x,y).
> 
>  
> 
> The product kind has a single constructor. But there is no way to
> express this at present that is safe.
> 
>  
> 
> As it stands, I can fake this to an extent in one direction, by writing
> 
>  
> 
> {-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures,
> MultiParamTypeClasses, PolyKinds, TypeFamilies,
> 
>              RankNTypes, TypeOperators, DefaultSignatures, DataKinds,
> 
>              FlexibleInstances, UndecidableInstances #-}
> 
>  
> 
> module Kmett where
> 
>  
> 
> type family Fst (p :: (a,b)) :: a
> 
> type instance Fst '(a,b) = a
> 
>  
> 
> type family Snd (p :: (a,b)) :: b
> 
> type instance Snd '(a,b) = b
> 
>  
> 
> data Thrist :: ((i,i) -> *) -> (i,i) -> * where
> 
>   Nil  :: Thrist a '(i,i)
> 
>   (:-) :: (Fst ij ~ i, Snd ij ~ j, Fst ik ~ i, Snd ik ~ k) =>
> 
>           a ij -> Thrist a '(j,k) -> Thrist a ik
> 
>  
> 
> irt :: a x -> Thrist a x
> 
> irt ax = ax :- Nil
> 
>  
> 
> and this compiles, but it just pushes the problem down the road, because
> with that I can show that given ij :: (x,y), I can build up a tuple
> '(Fst ij, Snd ij) :: (x,y)
> 
>  
> 
> But it doesn't give me that '(Fst ij, Snd ij) ~ ij, which you need later
> when you go to define an indexed bind, and type families are
> insufficient to the task. Right now to get this property I'm forced to
> fake it with unsafeCoerce.
> 
>  
> 
> -Edward
> 

_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Richard Eisenberg | 3 Sep 21:26 2012

Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?

On Sep 1, 2012, at 4:25 AM, Adam Gundry wrote:

> As Edward and others have recognised, the problem here is that FC
> coercions are not expressive enough to prove eta rules, that is
> 
> forall x : (a, b) . x ~ (Fst x, Snd x)
> 
> or more generally, that every element of a single-constructor (record)
> type is equal to the constructor applied to the projections.
> 
> It seems like it should be perfectly fine to assert such a thing as an
> axiom, though, ... unless
> you have Any (as Richard observed), in which case all bets are off. Why
> did you want Any again?

I don't necessarily want Any, but Any is already there, in GHC.Exts. (Though, Any has been helpful in other
type hackery exploits of mine...) So, any way of introducing eta-coercions will have to respect Any.

Intriguingly, the most recent published formulation of FC [1] leaves room for adding eta rules. The issue
is one of consistency: if we have a coercion g : forall k1. forall k2. forall x:(k1,k2). x ~ (Fst x, Snd x) and
the existence of Any : forall k.k, can we derive h : Int ~ Bool? In [1], the rules for consistency (from which
progress & preservation are proved) apply only to coercions at a base kind, either * or Constraint. So, our
eta coercion g is exempt from the consistency check -- it cannot make a system inconsistent. Thus, with or
without Any, the coercion g cannot lead to a program that crashes due to a type error.

So, it seems possible to introduce eta coercions into FC for all kinds containing only one type constructor
without sacrificing soundness. How the type inference engine/source Haskell triggers the use of these
coercions is another matter, but there doesn't seem to be anything fundamentally wrong with the idea.

Richard
Richard Eisenberg | 4 Sep 00:20 2012

Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?

Forgot to include the reference:

[1] B. A. Yorgey et al. "Giving Haskell a Promotion" (http://www.seas.upenn.edu/~sweirich/papers/tldi12.pdf)

On Sep 3, 2012, at 3:26 PM, Richard Eisenberg wrote:

> On Sep 1, 2012, at 4:25 AM, Adam Gundry wrote:
> 
>> As Edward and others have recognised, the problem here is that FC
>> coercions are not expressive enough to prove eta rules, that is
>> 
>> forall x : (a, b) . x ~ (Fst x, Snd x)
>> 
>> or more generally, that every element of a single-constructor (record)
>> type is equal to the constructor applied to the projections.
>> 
>> It seems like it should be perfectly fine to assert such a thing as an
>> axiom, though, ... unless
>> you have Any (as Richard observed), in which case all bets are off. Why
>> did you want Any again?
> 
> 
> I don't necessarily want Any, but Any is already there, in GHC.Exts. (Though, Any has been helpful in other
type hackery exploits of mine...) So, any way of introducing eta-coercions will have to respect Any.
> 
> Intriguingly, the most recent published formulation of FC [1] leaves room for adding eta rules. The issue
is one of consistency: if we have a coercion g : forall k1. forall k2. forall x:(k1,k2). x ~ (Fst x, Snd x) and
the existence of Any : forall k.k, can we derive h : Int ~ Bool? In [1], the rules for consistency (from which
progress & preservation are proved) apply only to coercions at a base kind, either * or Constraint. So, our
eta coercion g is exempt from the consistency check -- it cannot make a system inconsistent. Thus, with or
without Any, the coercion g cannot lead to a program that crashes due to a type error.
> 
> So, it seems possible to introduce eta coercions into FC for all kinds containing only one type
constructor without sacrificing soundness. How the type inference engine/source Haskell triggers the
use of these coercions is another matter, but there doesn't seem to be anything fundamentally wrong with
the idea.
> 
> Richard
Andrea Vezzosi | 4 Sep 04:28 2012
Picon

Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?

On Mon, Sep 3, 2012 at 9:26 PM, Richard Eisenberg <eir <at> cis.upenn.edu> wrote:
> [...]
> So, it seems possible to introduce eta coercions into FC for all kinds containing only one type
constructor without sacrificing soundness. How the type inference engine/source Haskell triggers the
use of these coercions is another matter, but there doesn't seem to be anything fundamentally wrong with
the idea.
>

A recent snapshot of ghc HEAD doesn't seem to agree:

{-# LANGUAGE GADTs, KindSignatures, PolyKinds, DataKinds,
TypeFamilies, ScopedTypeVariables, TypeOperators #-}

import GHC.Exts
import Unsafe.Coerce

data (:=:) :: k -> k -> * where
  Refl :: a :=: a

trans :: a :=: b -> b :=: c -> a :=: c
trans Refl Refl = Refl

type family Fst (x :: (a,b)) :: a
type family Snd (x :: (a,b)) :: b

type instance Fst '(a,b) = a
type instance Snd '(a,b) = b

eta :: x :=: '(Fst x, Snd x)
eta = unsafeCoerce Refl
-- ^^^ this is an acceptable way to simulate new coercions, i hope

type family Bad s t  (x :: (a,b)) :: *
type instance Bad s t '(a,b) = s
type instance Bad s t Any = t

refl_Any :: Any :=: Any
refl_Any = Refl

cong_Bad :: x :=: y -> Bad s t x :=: Bad s t y
cong_Bad Refl = Refl

s_eq_t :: forall (s :: *) (t :: *). s :=: t
s_eq_t = cong_Bad (trans refl_Any eta)

subst :: x :=: y -> x -> y
subst Refl x = x

coerce :: s -> t
coerce = subst s_eq_t

{-
GHCi, version 7.7.20120830: http://www.haskell.org/ghc/  :? for help
*Main> coerce (4.0 :: Double) :: (Int,Int)
(Segmentation fault
-}

-- Andrea Vezzosi
Richard Eisenberg | 4 Sep 04:59 2012

Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?

I retract my statement.

My mistake was that I looked at the definition for consistency in FC -- which correctly is agnostic to
non-base-kind coercions -- and applied it only to the set of coercion assumptions, not to any coercion
derivable from the assumptions. As Andrea's example shows, by assuming an eta coercion, it is possible to
derive an inconsistent coercion.

Examining the definition for FC consistency more closely, an eta coercion does not match to the form
allowed for coercion assumptions used to prove consistency. The proof, in [1], requires all assumptions
to have a type family application on the left-hand side. An eta coercion does not have a type family
application on either side, and so the consistency proof in [1] does not apply.

In light of this, it would seem that allowing eta coercions while retaining consistency would require some
more work.

Thanks for pointing out my mistake.
Richard

[1] S. Weirich et al. "Generative Type Abstraction and Type-level Computation."
(http://www.seas.upenn.edu/~sweirich/papers/popl163af-weirich.pdf)

On Sep 3, 2012, at 10:28 PM, Andrea Vezzosi wrote:

> On Mon, Sep 3, 2012 at 9:26 PM, Richard Eisenberg <eir <at> cis.upenn.edu> wrote:
>> [...]
>> So, it seems possible to introduce eta coercions into FC for all kinds containing only one type
constructor without sacrificing soundness. How the type inference engine/source Haskell triggers the
use of these coercions is another matter, but there doesn't seem to be anything fundamentally wrong with
the idea.
>> 
> 
> A recent snapshot of ghc HEAD doesn't seem to agree:
> 
> {-# LANGUAGE GADTs, KindSignatures, PolyKinds, DataKinds,
> TypeFamilies, ScopedTypeVariables, TypeOperators #-}
> 
> import GHC.Exts
> import Unsafe.Coerce
> 
> data (:=:) :: k -> k -> * where
>  Refl :: a :=: a
> 
> trans :: a :=: b -> b :=: c -> a :=: c
> trans Refl Refl = Refl
> 
> type family Fst (x :: (a,b)) :: a
> type family Snd (x :: (a,b)) :: b
> 
> type instance Fst '(a,b) = a
> type instance Snd '(a,b) = b
> 
> eta :: x :=: '(Fst x, Snd x)
> eta = unsafeCoerce Refl
> -- ^^^ this is an acceptable way to simulate new coercions, i hope
> 
> type family Bad s t  (x :: (a,b)) :: *
> type instance Bad s t '(a,b) = s
> type instance Bad s t Any = t
> 
> refl_Any :: Any :=: Any
> refl_Any = Refl
> 
> cong_Bad :: x :=: y -> Bad s t x :=: Bad s t y
> cong_Bad Refl = Refl
> 
> s_eq_t :: forall (s :: *) (t :: *). s :=: t
> s_eq_t = cong_Bad (trans refl_Any eta)
> 
> subst :: x :=: y -> x -> y
> subst Refl x = x
> 
> coerce :: s -> t
> coerce = subst s_eq_t
> 
> {-
> GHCi, version 7.7.20120830: http://www.haskell.org/ghc/  :? for help
> *Main> coerce (4.0 :: Double) :: (Int,Int)
> (Segmentation fault
> -}
> 
> -- Andrea Vezzosi
> 
Edward Kmett | 5 Sep 20:21 2012
Picon

Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?

I've come to think the culprit here is the fallacy that Any should inhabit every kind. 


I realize this is useful from an implementation perspective, but it has a number of far reaching consequences:

This means that a product kind isn't truly a product of two kinds. x * y, it winds up as a distinguishable x * y + 1, as Andrea has shown us happens because you can write a type family or MPTC with fundep that can match on Any.

A coproduct of two kinds x + y, isn't x + y, its x + y + 1. 

Kind level naturals aren't kind nats, they are nats + 1, and not even the one point compactification we get with lazy nats where you have an indistinguishable infinity added to the domain, but rather there is a distinguished atom to each kind under consideration.

I noticed that the polykindedness of Any is abused in the GHC.TypeLits to make fundeps determining a kind, but where else is it exploited?

-Edward

On Mon, Sep 3, 2012 at 10:59 PM, Richard Eisenberg <eir <at> cis.upenn.edu> wrote:
I retract my statement.

My mistake was that I looked at the definition for consistency in FC -- which correctly is agnostic to non-base-kind coercions -- and applied it only to the set of coercion assumptions, not to any coercion derivable from the assumptions. As Andrea's example shows, by assuming an eta coercion, it is possible to derive an inconsistent coercion.

Examining the definition for FC consistency more closely, an eta coercion does not match to the form allowed for coercion assumptions used to prove consistency. The proof, in [1], requires all assumptions to have a type family application on the left-hand side. An eta coercion does not have a type family application on either side, and so the consistency proof in [1] does not apply.

In light of this, it would seem that allowing eta coercions while retaining consistency would require some more work.

Thanks for pointing out my mistake.
Richard

[1] S. Weirich et al. "Generative Type Abstraction and Type-level Computation."
(http://www.seas.upenn.edu/~sweirich/papers/popl163af-weirich.pdf)

On Sep 3, 2012, at 10:28 PM, Andrea Vezzosi wrote:

> On Mon, Sep 3, 2012 at 9:26 PM, Richard Eisenberg <eir <at> cis.upenn.edu> wrote:
>> [...]
>> So, it seems possible to introduce eta coercions into FC for all kinds containing only one type constructor without sacrificing soundness. How the type inference engine/source Haskell triggers the use of these coercions is another matter, but there doesn't seem to be anything fundamentally wrong with the idea.
>>
>
> A recent snapshot of ghc HEAD doesn't seem to agree:
>
> {-# LANGUAGE GADTs, KindSignatures, PolyKinds, DataKinds,
> TypeFamilies, ScopedTypeVariables, TypeOperators #-}
>
> import GHC.Exts
> import Unsafe.Coerce
>
> data (:=:) :: k -> k -> * where
>  Refl :: a :=: a
>
> trans :: a :=: b -> b :=: c -> a :=: c
> trans Refl Refl = Refl
>
> type family Fst (x :: (a,b)) :: a
> type family Snd (x :: (a,b)) :: b
>
> type instance Fst '(a,b) = a
> type instance Snd '(a,b) = b
>
> eta :: x :=: '(Fst x, Snd x)
> eta = unsafeCoerce Refl
> -- ^^^ this is an acceptable way to simulate new coercions, i hope
>
> type family Bad s t  (x :: (a,b)) :: *
> type instance Bad s t '(a,b) = s
> type instance Bad s t Any = t
>
> refl_Any :: Any :=: Any
> refl_Any = Refl
>
> cong_Bad :: x :=: y -> Bad s t x :=: Bad s t y
> cong_Bad Refl = Refl
>
> s_eq_t :: forall (s :: *) (t :: *). s :=: t
> s_eq_t = cong_Bad (trans refl_Any eta)
>
> subst :: x :=: y -> x -> y
> subst Refl x = x
>
> coerce :: s -> t
> coerce = subst s_eq_t
>
> {-
> GHCi, version 7.7.20120830: http://www.haskell.org/ghc/  :? for help
> *Main> coerce (4.0 :: Double) :: (Int,Int)
> (Segmentation fault
> -}
>
> -- Andrea Vezzosi
>


_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Richard Eisenberg | 5 Sep 20:58 2012

Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?


On Sep 5, 2012, at 2:21 PM, Edward Kmett wrote:

I noticed that the polykindedness of Any is abused in the GHC.TypeLits to make fundeps determining a kind, but where else is it exploited?

I similarly abused Any to write the singletons library, but it's really a hack to work with kind classes and functions from kinds to types. If these features were directly accessible, the Any hack would no longer be needed.

Has anyone out there used Any for another purpose?

Richa rd
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Simon Peyton-Jones | 16 Sep 17:49 2012
Picon

RE: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?

Friends

Thanks for this useful conversation, by email and at ICFP.  Here's my summary.  Please tell me if I'm on the
right track.  It would be great if someone wanted to create a page on the GHC wiki to capture the issues and outcomes.

Simon

Eta rules
~~~~~~
*   We want to add eta-rules to FC.  Sticking to pairs for now, that would amount to
     adding two new type functions (Fst, Snd), and three new, built-in axioms
	axPair k1 k2 (a:'(k1,k2)) : a ~ '(Fst a, Snd a)
	axFst k1 k2 (a:k1) (b:k2) : Fst '(a,b) ~ a
	axSnd k1 k2 (a:k1) (b:k2) : Snd '(a,b) ~ a
     Generalising to arbitrary products looks feasible.

*  Adding these axioms would make FC inconsistent, because 
	axPair * * (Any '(*,*) ) : Any '(*,*) ~ (Fst .., Snd ..)
     and that has two different type constructors on each side.
     However, I think is readily solved: see below under "Fixing Any"

* Even in the absence of Any, it's not 100% obvious that adding the above
   eta axioms retains consistency of FC.  I believe that Richard is volunteering
   to check this out.  Right, Richard?

Type inference
~~~~~~~~~
I'm a little unclear about the implications for inference.  One route
might be this.   Suppose we are trying to solve a constraint
     [W]  (a:'(k1,ks)) ~ '( t1, t2 )
where a is an untouchable type variable.  (if it was touchable we'd
simply unify it.)  Then we can replace it with a constraint
    [W]   '(Fst a, Snd a) ~ '( t1, t2)

Is that it?  Or do we need more?  I'm a bit concerned about constraints like
    F a ~ e
where a:'(k1,k2), and we have a type instance like  F '(a,b) = ...

Anything else?

I don't really want to eagerly eta-expand every type variable, because (a) we'll bloat the constraints and
(b) we might get silly error messages.  For (b) consider the insoluble constraint
    [W]  a~b
where a and b are both skolems of kind '(k1,k2). If we eta-expand both we'll get two insoluble constraints
(Fst a ~ Fst b) and (Snd a ~ Snd b), and we DEFINITELY don't want to report that as a type error!

Fixing Any
~~~~~~~
* I think we can fix the Any problem readily by making Any into a type family, 
     that has no instances.   We certainly allow equalities with a type
     *family* application on the left and a type constructor on the right.
     I have implemented this change already... it seems like a good plan.
	
* Several people have asked why we need Any at all.  Consider this source program
         reverse []
     At what type should we instantiate 'reverse' and the empty list []?  Any type
     will do, but we must choose one; FC doesn't have unbound type variables.
     So I instantiate it at (Any *):
         reverse (Any *) ([] (Any *))

     Why is Any poly-kinded?  Because the above ambiguity situation sometimes 
     arises at other kinds.

*   I'm betting that making Any into a family will mess up Richard's (entirely separate)
     use of (Any k) as a proxy for a kind argument k; because now (Any k1 ~ Any k2)
     does not entail (k1~k2).   We need Any to be an *injective* type family.  We want
     injective type families anyway, so I guess I should add the internal machinery 
     (which is easy).

     I believe that injective type families are fully decomposable, just like data type families,
     correct?  To make them available at the source level, we'd just need to
       a) add the syntax     injective type family F a :: *
       b) check for injectivity when the user adds type instances
     Richard, would you like to do that part?
Gábor Lehel | 18 Sep 08:54 2012
Picon

Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?

On Sun, Sep 16, 2012 at 5:49 PM, Simon Peyton-Jones
<simonpj <at> microsoft.com> wrote:
>
> Fixing Any
> ~~~~~~~
> * I think we can fix the Any problem readily by making Any into a type family,
>      that has no instances.   We certainly allow equalities with a type
>      *family* application on the left and a type constructor on the right.
>      I have implemented this change already... it seems like a good plan.
>

Will unsafeCoercing to and from Any still work with this plan? (If not
then I can just use data Anything = forall a. Anything a, so it's not
a big deal.)

--

-- 
Your ship was destroyed in a monadic eruption.
Simon Peyton-Jones | 18 Sep 09:11 2012
Picon

RE: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?

| Will unsafeCoercing to and from Any still work with this plan? (If not
| then I can just use data Anything = forall a. Anything a, so it's not a
| big deal.)

Yes I think it'll be fine, but thanks for highlighting this other use of Any.

Simon
Simon Peyton-Jones | 18 Sep 09:10 2012
Picon

RE: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?

I think I was a little hasty below, and need a little help.

Making 'Any' an type family, even an injective one, does not work for the use that Richard and Iavor make of
it, eg in TypeLits.  Here's an example from TypeLits:

	instance SingE (Any :: Nat) Integer where
where SingE :: forall k. k -> * -> Constraint

Here Iavor is using Any as a proxy kind argument.  He really wants
	SingE :: forall k. * -> Constraint
with kind-indexed instances. But (much as with the Typeable class at the value level) he is giving it a type
argument so that he can later say things like
	SingE (Any :: *->*) v
Without this trick we'd need kind application, something like
	SingE {*->*} v

None of this works if Any is a type family, because the type patterns in an instance decl aren't allowed to
involve type families (and rightly so; value declarations don't have functions in patterns).

Nor can we fix this by introducing some *other* constant, Proxy :: forall k. k, because that suffers from the
inconsistency problem that we started with.  Another way to say this is as follows.  In the value world we
have often written
	typeOf (undefined :: a)
using bottom as a proxy type argument. That works in Haskell, but not in a strict, or strongly-normalising
language.  And at the type level we are (mostly) strongly normalising.

The technically-straightforward thing to do is to add kind application, but that's a bit complicated
notationally.  http://hackage.haskell.org/trac/ghc/wiki/ExplicitTypeApplication   Does anyone
have any other ideas?

Simon

| -----Original Message-----
| From: Simon Peyton-Jones
| Sent: 16 September 2012 16:49
| To: Richard Eisenberg; Andrea Vezzosi
| Cc: Adam Gundry; Conor McBride; Stephanie Weirich; glasgow-haskell-
| users <at> haskell.org; Simon Peyton-Jones
| Subject: RE: PolyKind issue in GHC 7.6.1rc1: How to make a kind a
| functional dependency?
| 
| Friends
| 
| Thanks for this useful conversation, by email and at ICFP.  Here's my
| summary.  Please tell me if I'm on the right track.  It would be great
| if someone wanted to create a page on the GHC wiki to capture the issues
| and outcomes.
| 
| Simon
| 
| Eta rules
| ~~~~~~
| *   We want to add eta-rules to FC.  Sticking to pairs for now, that
| would amount to
|      adding two new type functions (Fst, Snd), and three new, built-in
| axioms
| 	axPair k1 k2 (a:'(k1,k2)) : a ~ '(Fst a, Snd a)
| 	axFst k1 k2 (a:k1) (b:k2) : Fst '(a,b) ~ a
| 	axSnd k1 k2 (a:k1) (b:k2) : Snd '(a,b) ~ a
|      Generalising to arbitrary products looks feasible.
| 
| *  Adding these axioms would make FC inconsistent, because
| 	axPair * * (Any '(*,*) ) : Any '(*,*) ~ (Fst .., Snd ..)
|      and that has two different type constructors on each side.
|      However, I think is readily solved: see below under "Fixing Any"
| 
| * Even in the absence of Any, it's not 100% obvious that adding the
| above
|    eta axioms retains consistency of FC.  I believe that Richard is
| volunteering
|    to check this out.  Right, Richard?
| 
| Type inference
| ~~~~~~~~~
| I'm a little unclear about the implications for inference.  One route
| might be this.   Suppose we are trying to solve a constraint
|      [W]  (a:'(k1,ks)) ~ '( t1, t2 )
| where a is an untouchable type variable.  (if it was touchable we'd
| simply unify it.)  Then we can replace it with a constraint
|     [W]   '(Fst a, Snd a) ~ '( t1, t2)
| 
| Is that it?  Or do we need more?  I'm a bit concerned about constraints
| like
|     F a ~ e
| where a:'(k1,k2), and we have a type instance like  F '(a,b) = ...
| 
| Anything else?
| 
| I don't really want to eagerly eta-expand every type variable, because
| (a) we'll bloat the constraints and (b) we might get silly error
| messages.  For (b) consider the insoluble constraint
|     [W]  a~b
| where a and b are both skolems of kind '(k1,k2). If we eta-expand both
| we'll get two insoluble constraints (Fst a ~ Fst b) and (Snd a ~ Snd b),
| and we DEFINITELY don't want to report that as a type error!
| 
| Fixing Any
| ~~~~~~~
| * I think we can fix the Any problem readily by making Any into a type
| family,
|      that has no instances.   We certainly allow equalities with a type
|      *family* application on the left and a type constructor on the
| right.
|      I have implemented this change already... it seems like a good
| plan.
| 
| * Several people have asked why we need Any at all.  Consider this
| source program
|          reverse []
|      At what type should we instantiate 'reverse' and the empty list []?
| Any type
|      will do, but we must choose one; FC doesn't have unbound type
| variables.
|      So I instantiate it at (Any *):
|          reverse (Any *) ([] (Any *))
| 
|      Why is Any poly-kinded?  Because the above ambiguity situation
| sometimes
|      arises at other kinds.
| 
| *   I'm betting that making Any into a family will mess up Richard's
| (entirely separate)
|      use of (Any k) as a proxy for a kind argument k; because now (Any
| k1 ~ Any k2)
|      does not entail (k1~k2).   We need Any to be an *injective* type
| family.  We want
|      injective type families anyway, so I guess I should add the
| internal machinery
|      (which is easy).
| 
|      I believe that injective type families are fully decomposable, just
| like data type families,
|      correct?  To make them available at the source level, we'd just
| need to
|        a) add the syntax     injective type family F a :: *
|        b) check for injectivity when the user adds type instances
|      Richard, would you like to do that part?
Iavor Diatchki | 18 Sep 16:07 2012
Picon

Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?

Hello,


On Tue, Sep 18, 2012 at 12:10 AM, Simon Peyton-Jones <simonpj <at> microsoft.com> wrote:

The technically-straightforward thing to do is to add kind application, but that's a bit complicated notationally.  http://hackage.haskell.org/trac/ghc/wiki/ExplicitTypeApplication   Does anyone have any other ideas?


I think that the right way to proceed would be to add explicit syntax for kind abstraction and application (which, I imagine, we already have internally in GHC).  As for the concrete syntax, I prefer the explicitly annotated form, even if the ":: Kind" part is treated completely syntactically for the moment, because the notation seems compatible with future generalizations that we might want to do (e.g., the work that Stephanie, Richard, Connor, and Adam are doing).  So the source Haskell might look something like this:

type family SingRep (a :: Kind)
type instance SingRep (Nat :: Kind) = Integer

class SingE (a :: Kind) where ...


-Iavor
PS: I just modified the ExplicitTypeApplication wiki page to reflect more accurately the singletons example.  For those who've seen the old page:  I changed the 'Sing' data family example, because that family needs an actual type parameter---it is not enough to just have a kind parameter (the reason being that we want to write things like "Sing 5", where "5" is a type).









_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Andrea Vezzosi | 19 Sep 19:26 2012
Picon

Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?

On Sun, Sep 16, 2012 at 5:49 PM, Simon Peyton-Jones
<simonpj <at> microsoft.com> wrote:
> [...]
> Type inference
> ~~~~~~~~~
> I'm a little unclear about the implications for inference.  One route
> might be this.   Suppose we are trying to solve a constraint
>      [W]  (a:'(k1,ks)) ~ '( t1, t2 )
> where a is an untouchable type variable.  (if it was touchable we'd
> simply unify it.)  Then we can replace it with a constraint
>     [W]   '(Fst a, Snd a) ~ '( t1, t2)
>
> Is that it?  Or do we need more?  I'm a bit concerned about constraints like
>     F a ~ e
> where a:'(k1,k2), and we have a type instance like  F '(a,b) = ...
>

F a ~ F '(Fst a, Snd a) has to hold, so one does need to expand a for
constraints like F a ~ e in this case. One way to think of it is that
patterns like '(a,b) are the same as value-level ~(a,b) ones.

-- Andrea
Richard Eisenberg | 19 Sep 20:51 2012

Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?

Please see my responses inline.

On Sep 16, 2012, at 11:49 AM, Simon Peyton-Jones wrote:

> Eta rules
> ~~~~~~
> *   We want to add eta-rules to FC.  Sticking to pairs for now, that would amount to
>     adding two new type functions (Fst, Snd), and three new, built-in axioms
> 	axPair k1 k2 (a:'(k1,k2)) : a ~ '(Fst a, Snd a)
> 	axFst k1 k2 (a:k1) (b:k2) : Fst '(a,b) ~ a
> 	axSnd k1 k2 (a:k1) (b:k2) : Snd '(a,b) ~ a
>     Generalising to arbitrary products looks feasible.

The last two axioms are the straightforward compilations of the type families Fst and Snd -- nothing new is
needed to create these. The first is the challenge and will require some type inference magic.

> 
> *  Adding these axioms would make FC inconsistent, because 
> 	axPair * * (Any '(*,*) ) : Any '(*,*) ~ (Fst .., Snd ..)
>     and that has two different type constructors on each side.
>     However, I think is readily solved: see below under "Fixing Any"
> 
> * Even in the absence of Any, it's not 100% obvious that adding the above
>   eta axioms retains consistency of FC.  I believe that Richard is volunteering
>   to check this out.  Right, Richard?

I'll be going through the consistency proof shortly for some other work I'm doing, so I'll throw this into
the mix while it's all paged in. This might be tricky, though.

> 
> Type inference
> ~~~~~~~~~
> I'm a little unclear about the implications for inference.  One route
> might be this.   Suppose we are trying to solve a constraint
>     [W]  (a:'(k1,ks)) ~ '( t1, t2 )
> where a is an untouchable type variable.  (if it was touchable we'd
> simply unify it.)  Then we can replace it with a constraint
>    [W]   '(Fst a, Snd a) ~ '( t1, t2)

I don't think that's the right replacement. The next natural step would be decomposition, leading to (Fst a
~ t1) and (Snd a ~ t2), which would then get stuck, because Fst and Snd  aren't injective. So, I would say we need

  a1, a2 fresh
  [G] a ~ '(a1, a2)
  [W] '(a1, a2) ~ '(t1, t2)

which would then decompose correctly. As I write this, I'm worried about that freshness condition… what
if 'a' appears multiple times in the type? We would either need to guarantee that a1 and a2 are the same each
time, or create new [W] constraints that a1 ~ a1', etc. But, maybe this is easier in practice than it seems.
Type inference experts?

> 
> Is that it?  Or do we need more?  I'm a bit concerned about constraints like
>    F a ~ e
> where a:'(k1,k2), and we have a type instance like  F '(a,b) = …

Here, the proper eta-expansion (a ~ '(Fst a, Snd a)) works great, no?

> 
> Anything else?
> 
> I don't really want to eagerly eta-expand every type variable, because (a) we'll bloat the constraints
and (b) we might get silly error messages.  For (b) consider the insoluble constraint
>    [W]  a~b
> where a and b are both skolems of kind '(k1,k2). If we eta-expand both we'll get two insoluble constraints
(Fst a ~ Fst b) and (Snd a ~ Snd b), and we DEFINITELY don't want to report that as a type error!

Could this be handled using mechanisms already in place to report errors about unexpanded type synonyms?
If so, we could eagerly expand, and I think that would ease the implementation. However, I defer to those
more expert than I in such issues.

> 
> Fixing Any
> ~~~~~~~
> * I think we can fix the Any problem readily by making Any into a type family, 
>     that has no instances.   We certainly allow equalities with a type
>     *family* application on the left and a type constructor on the right.
>     I have implemented this change already... it seems like a good plan.
> 	
> * Several people have asked why we need Any at all.  Consider this source program
>         reverse []
>     At what type should we instantiate 'reverse' and the empty list []?  Any type
>     will do, but we must choose one; FC doesn't have unbound type variables.
>     So I instantiate it at (Any *):
>         reverse (Any *) ([] (Any *))
> 
>     Why is Any poly-kinded?  Because the above ambiguity situation sometimes 
>     arises at other kinds.
> 
> *   I'm betting that making Any into a family will mess up Richard's (entirely separate)
>     use of (Any k) as a proxy for a kind argument k; because now (Any k1 ~ Any k2)
>     does not entail (k1~k2).   We need Any to be an *injective* type family.  We want
>     injective type families anyway, so I guess I should add the internal machinery 
>     (which is easy).

I don't think injectivity is the key here. As I understand it, any equality t1 ~ t2 entails k1 ~ k2, where t1:k1
and t2:k2. When trying to unify Any k1 ~ Any k2, GHC will already (I think) unify k1 and k2, just based on the
kinds, not on injectivity. Is there something here I'm missing?

> 
>     I believe that injective type families are fully decomposable, just like data type families,
>     correct?

No, I don't think so. Data families are generative, which is a stronger condition than injective. Consider
(D a ~ b c), where D is a data family (or a constructor, for that matter). Then, we can surely decompose to (D ~
b, a ~ c). However, the same is not true for type families. If we have (F a ~ b c), we can't go further, even if F is
injective. If we have (F a ~ F b), where we know F is injective, then we can decompose to (a ~ b), but that's the
only gain we get.

>  To make them available at the source level, we'd just need to
>       a) add the syntax     injective type family F a :: *
>       b) check for injectivity when the user adds type instances
>     Richard, would you like to do that part?
> 

A long, long time ago, I volunteered to look at injectivity of type functions. That task it quite literally
on my todo list, but it feels like I'm getting through a long season of putting out fires, and injectivity
hasn't been burning brightly enough. I think the last of the brightly-burning ones will either be
extinguished or go out on its own on October 8 (PLPV deadline). After that date, I'll have more of a chance to
look at this. 

Simon, if you add the internal machinery, I'm happy to do the external stuff -- shouldn't be hard.

> 
> 

As for recovering "kind classes" and such once Any is made into a type family: I'm in favor of finding some way
to do explicit kind instantiation, making the Any trick obsolete. I'm happy to leave it to others to decide
the best concrete syntax.

Richard
Nicolas Frisby | 12 Oct 05:20 2012
Picon

Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?

On Wed, Sep 19, 2012 at 1:51 PM, Richard Eisenberg <eir <at> cis.upenn.edu> wrote:
> As for recovering "kind classes" and such once Any is made into a type family: I'm in favor of finding some
way to do explicit kind instantiation, making the Any trick obsolete. I'm happy to leave it to others to
decide the best concrete syntax.

I'll admit I haven't parsed this entire email thread, but I read
enough of it early on that I wanted to avoid Any recently. Returning
to find this quote from Richard, perhaps the trick I came up is the
one you're after.

(Also — what's the general status on this initiative? Has much
happened in about a month?)

The to my trick key is to use the promotion of this data type.

> data KindProxy (k :: *) = KindProxy

I needed it in order to define this family, which counts the number of
arguments a kind has.

> type family CountArgs (kp :: KindProxy k) :: Nat
> type instance CountArgs (kp :: *) = Z
> type instance CountArgs (kp :: kD -> kR) = S (CountArgs ('KindProxy :: KindProxy kR))

The proxy is necessary on the RHS of the second instance, in which I
need a type of kind kR, but I wouldn't have any means to build one
(without Any) were CountArgs simply of kind (k -> Nat).

This usage is comparable to Richard's usage in the singletons library,
insomuch as I understand from the Haskell 2012 paper.

I'm less familiar with the usage in GHC.TypeLits. At a quick glance, I
believe I'd change SingE like so

> class SingE (kparam :: KindProxy k) rep | kparam -> rep where
>   fromSing :: Sing (a :: k) -> rep

> instance SingE (kparam :: KindProxy Nat) Integer where
>   fromSing (SNat n) = n

> instance SingE (kparam :: KindProxy Symbol) String where
>   fromSing (SSym s) = s

However, looking through the rest of that module, I see no point where
a proxy is actually required (as it is required in the second case of
CountArgs). Maybe I'm just missing it, or maybe Iavor is just
interested in *enforcing* the fact that the type is not of
consequence?

Along those same lines… Iavor had SingE instances declared for (Any ::
KindProxy Nat) and (Any :: KindProxy Symbol). I'm not sure why he
didn't leave the type polymorphic, as I have. Perhaps it matters for
various uses of SingE? I haven't tried using my code with examples, so
maybe that's where issues would show up. If it were necessary, the
instances could instead be as follows.

> instance SingE ('KindProxy :: KindProxy Nat) Integer where
>   fromSing (SNat n) = n

> instance SingE ('KindProxy :: KindProxy Symbol) String where
>   fromSing (SSym s) = s

Is this the kind of trick you were after, Richard? It might pollute
the code base and interface a bit with KindProxy wrappers, but I've
not found that insurmountable. Hopefully that isn't a show stopper for
you.

HTH
Nicolas Frisby | 12 Oct 05:21 2012
Picon

Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?

On Thu, Oct 11, 2012 at 10:20 PM, Nicolas Frisby
<nicolas.frisby <at> gmail.com> wrote:
> The to my trick key is to use the promotion of this data type.

"The key to my trick is to use the promotion of this data type."

Wow — I have no idea what happened there.
Richard Eisenberg | 12 Oct 05:47 2012

Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?


On Oct 11, 2012, at 11:20 PM, Nicolas Frisby wrote:
> 
> (Also — what's the general status on this initiative? Has much
> happened in about a month?)

From my end, nothing. I'm trying to wrap up some other work I'm doing on GHC (ordered overlapping type family
instances), and it looks like some of the questions I raised in my last email in this thread are still open.

> 
> The to my trick key is to use the promotion of this data type.
> 
>> data KindProxy (k :: *) = KindProxy

Yes, I used this in an earlier version of singletons. Then, Simon told me about Any, and that cleaned up the
code considerably. I don't think, though, there was anything fundamentally wrong (other than
aesthetics) with KindProxy. Thanks for bringing this up, as I had forgotten about this approach in the
intervening months.
> 
> I'm less familiar with the usage in GHC.TypeLits.

Iavor and I collaborated on the design of the building blocks of singleton types, as we wanted our work to be
interoperable. A recent scan through TypeLits tells me, though, that somewhere along the way, our
designs diverged a bit. Somewhere on the to-do list is to re-unify the interfaces, and actually just to
import TypeLits into Data.Singletons so the definitions are one and the same. Iavor, I'm happy to talk
about the details if you are.

Nick, thanks for pushing on this thread!

Richard
Simon Peyton-Jones | 12 Oct 18:51 2012
Picon

RE: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?

| Iavor and I collaborated on the design of the building blocks of
| singleton types, as we wanted our work to be interoperable. A recent
| scan through TypeLits tells me, though, that somewhere along the way,
| our designs diverged a bit. Somewhere on the to-do list is to re-unify
| the interfaces, and actually just to import TypeLits into
| Data.Singletons so the definitions are one and the same. Iavor, I'm
| happy to talk about the details if you are.

That would be good!

Simon
Simon Peyton-Jones | 12 Oct 18:51 2012
Picon

RE: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?

| > (Also - what's the general status on this initiative? Has much
| > happened in about a month?)
| 
| From my end, nothing. I'm trying to wrap up some other work I'm doing
| on GHC (ordered overlapping type family instances), and it looks like
| some of the questions I raised in my last email in this thread are
| still open.

I think "this initiative" refers to the question of eta expansion in FC.  

We are stalled on this, partly for lack of bandwidth and partly because there are more urgent things to do. 
But I did capture the issue in this ticket
	http://hackage.haskell.org/trac/ghc/ticket/7259

Simon
Dan Doel | 20 Sep 01:24 2012
Picon

Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?

On Sun, Sep 16, 2012 at 11:49 AM, Simon Peyton-Jones
<simonpj <at> microsoft.com> wrote:
> I don't really want to eagerly eta-expand every type variable, because (a) we'll bloat the constraints
and (b) we might get silly error messages.  For (b) consider the insoluble constraint
>     [W]  a~b
> where a and b are both skolems of kind '(k1,k2). If we eta-expand both we'll get two insoluble constraints
(Fst a ~ Fst b) and (Snd a ~ Snd b), and we DEFINITELY don't want to report that as a type error!

I almost forgot to mention this, but...

You should perhaps talk to the agda implementors. They've done a lot
of work to avoid eta expanding as much as possible, because it was
killing performance (but it does also make for some nicer display). So
they probably know some tricks.

-- Dan
Simon Peyton-Jones | 31 Aug 18:59 2012
Picon

RE: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?

Same question.  Do you expect the code below to type-check?  I have stripped it down to essentials.  Currently it’s rejected with

 

    Couldn't match type `a' with '(,) k k1 b0 d0

 

And that seems reasonable, doesn’t it?  After all, in the defn of bidStar, (:*) returns a value of type

     Star x y ‘(a,c) ‘(b,d)

which is manifestly incompatible with the claimed, more polymorphic type.  And this is precisely the same error as comes from your class/instance example below, and for precisely the same reason. 

 

I must be confused.

 

Simon

 

                                                                                                                                       

{-# LANGUAGE PolyKinds, DataKinds, TypeOperators, GADTs #-}

module Product where

 

data Star :: (x -> x -> *) -> (y -> y -> *) -> (x,y) -> (x,y) -> * where

  (:*) :: x a b -> y c d -> Star x y '(a,c) '(b,d)

 

bidStar :: Star T T a a

bidStar = bidT :* bidT

 

data T a b = MkT

 

bidT :: T a a

bidT = MkT

 

From: Edward Kmett [mailto:ekmett <at> gmail.com]
Sent: 31 August 2012 13:45
To: Simon Peyton-Jones
Cc: glasgow-haskell-users <at> haskell.org
Subject: Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?

 

Hrmm. This seems to render product kinds rather useless, as there is no way to refine the code to reflect the knowledge that they are inhabited by a single constructor. =( 

 

For instance, there doesn't even seem to be a way to make the following code compile, either.

 

 

{-# LANGUAGE PolyKinds, DataKinds, TypeOperators, GADTs #-}

module Product where

 

import Prelude hiding (id,(.))

 

class Category k where

  id :: k a a

  (.) :: k b c -> k a b -> k a c

 

data (*) :: (x -> x -> *) -> (y -> y -> *) -> (x,y) -> (x,y) -> * where

  (:*) :: x a b -> y c d -> (x * y) '(a,c) '(b,d)

 

instance (Category x, Category y) => Category (x * y) where

  id = id :* id

  (xf :*  yf) . (xg :* yg) = (xf . xg) :* (yf . yg)

 

This all works perfectly fine in Conor's SHE, (as does the thrist example) so I'm wondering where the impedence mismatch comes in and how to gain knowledge of this injectivity to make it work.

 

Also, does it ever make sense for the kind of a kind variable mentioned in a type not to get a functional dependency on the type? 

 

e.g. should

 

class Foo (m :: k -> *)

 

always be

 

class Foo (m :: k -> *) | m -> k

 

?

 

Honest question. I can't come up with a scenario, but you might have one I don't know.

 

-Edward

 

On Fri, Aug 31, 2012 at 5:55 AM, Simon Peyton-Jones <simonpj <at> microsoft.com> wrote:

With the code below, I get this error message with HEAD. And that looks right to me, no?

The current 7.6 branch gives the same message printed less prettily.

 

If I replace the defn of irt with

irt :: a '(i,j) -> Thrist a '(i,j)

irt ax = ax :- Nil

 

then it typechecks.

 

Simon

 

 

Knett.hs:20:10:

    Couldn't match type `x' with '(i0, k0)

      `x' is a rigid type variable bound by

          the type signature for irt :: a x -> Thrist k a x at Knett.hs:19:8

    Expected type: Thrist k a x

      Actual type: Thrist k a '(i0, k0)

    In the expression: ax :- Nil

    In an equation for `irt': irt ax = ax :- Nil

simonpj <at> cam-05-unx:~/tmp$

 

 

{-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures, MultiParamTypeClasses, PolyKinds,

             RankNTypes, TypeOperators, DefaultSignatures, DataKinds,

             FlexibleInstances, UndecidableInstances #-}

 

module Knett where

 

class IMonad (m :: (k -> *) -> k -> *) | m -> k where

  ireturn :: a x -> m a x

 

infixr 5 :-

 

data Thrist :: ((i,i) -> *) -> (i,i) -> * where

  Nil  :: Thrist a '(i,i)

  (:-) :: a '(i,j) -> Thrist a '(j,k) -> Thrist a '(i,k)

 

-- instance IMonad Thrist where

--  ireturn a = a :- Nil

 

irt :: a x -> Thrist a x

irt ax = ax :- Nil

 

 

From: glasgow-haskell-users-bounces <at> haskell.org [mailto:glasgow-haskell-users-bounces <at> haskell.org] On Behalf Of Edward Kmett
Sent: 31 August 2012 03:38
To: glasgow-haskell-users <at> haskell.org
Subject: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?

 

If I define the following

 

{-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures, MultiParamTypeClasses, PolyKinds, RankNTypes, TypeOperators, DefaultSignatures, DataKinds, FlexibleInstances, UndecidableInstances #-}

module Indexed.Test where

 

class IMonad (m :: (k -> *) -> k -> *) where 

  ireturn :: a x -> m a x

 

infixr 5 :-

data Thrist :: ((i,i) -> *) -> (i,i) -> * where

  Nil :: Thrist a '(i,i)

  (:-) :: a '(i,j) -> Thrist a '(j,k) -> Thrist a '(i,k)

 

instance IMonad Thrist where

  ireturn a = a :- Nil

 

Then 'ireturn' complains (correctly) that it can't match the k with the kind (i,i). The reason it can't is because when you look at the resulting signature for the MPTC it generates it looks like

 

class IMonad k m where

  ireturn :: a x -> m a x

 

However, there doesn't appear to be a way to say that the kind k should be determined by m. 

 

I tried doing:

 

class IMonad (m :: (k -> *) -> k -> *) | m -> k where 

  ireturn :: a x -> m a x

 

Surprisingly (to me) this compiles and generates the correct constraints for IMonad:

 

ghci> :set -XPolyKinds -XKindSignatures -XFunctionalDependencies -XDataKinds -XGADTs

ghci> class IMonad (m :: (k -> *) -> k -> *) | m -> k where ireturn :: a x -> m a x

ghci> :info IMonad

class IMonad k m | m -> k where

  ireturn :: a x -> m a x

 

But when I add 

 

ghci> :{

Prelude| data Thrist :: ((i,i) -> *) -> (i,i) -> * where

Prelude|   Nil :: Thrist a '(i,i)

Prelude|   (:-) :: a '(i,j) -> Thrist a '(j,k) -> Thrist a '(i,k)

Prelude| :}

 

and attempt to introduce the instance, I crash:

 

ghci> instance IMonad Thrist where ireturn a = a :- Nil

ghc: panic! (the 'impossible' happened)

  (GHC version 7.6.0.20120810 for x86_64-apple-darwin):

    lookupVarEnv_NF: Nothing

 

Please report this as a GHC bug:  http://www.haskell.org/ghc/reportabug

 

Moreover, attempting to compile them in separate modules leads to a different issue. 

 

Within the module, IMonad has a type that includes the kind k and the constraint on it from m. But from the other module, :info shows no such constraint, and the above code again fails to typecheck, but upon trying to recompile, when GHC goes to load the IMonad instance from the core file, it panicks again differently about references to a variable not present in the core.

 

Is there any way to make such a constraint that determines a kind from a type parameter in GHC 7.6 at this time?

 

I tried the Kind hack used in GHC.TypeLits, but it doesn't seem to be applicable to this situation.

 

-Edward

 

_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Simon Peyton-Jones | 31 Aug 18:45 2012
Picon

RE: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?

Hrmm. This seems to render product kinds rather useless, as there is no way to refine the code to reflect the knowledge that they are inhabited by a single constructor. =( 

 

Wait. When you say “This seems to render produce kinds useless”, are you saying that in the code I wrote, you think irt should compile??  I reproduce it below for completeness.

 

Simon

 

{-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures, MultiParamTypeClasses, PolyKinds,

             RankNTypes, TypeOperators, DefaultSignatures, DataKinds,

             FlexibleInstances, UndecidableInstances #-}

 

module Knett where

 

data Thrist :: ((i,i) -> *) -> (i,i) -> * where

  Nil  :: Thrist a '(i,i)

  (:-) :: a '(i,j) -> Thrist a '(j,k) -> Thrist a '(i,k)

 

irt :: a x -> Thrist a x

irt ax = ax :- Nil

 

 

From: Edward Kmett [mailto:ekmett <at> gmail.com]
Sent: 31 August 2012 13:45
To: Simon Peyton-Jones
Cc: glasgow-haskell-users <at> haskell.org
Subject: Re: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?

 

Hrmm. This seems to render product kinds rather useless, as there is no way to refine the code to reflect the knowledge that they are inhabited by a single constructor. =( 

 

For instance, there doesn't even seem to be a way to make the following code compile, either.

 

 

{-# LANGUAGE PolyKinds, DataKinds, TypeOperators, GADTs #-}

module Product where

 

import Prelude hiding (id,(.))

 

class Category k where

  id :: k a a

  (.) :: k b c -> k a b -> k a c

 

data (*) :: (x -> x -> *) -> (y -> y -> *) -> (x,y) -> (x,y) -> * where

  (:*) :: x a b -> y c d -> (x * y) '(a,c) '(b,d)

 

instance (Category x, Category y) => Category (x * y) where

  id = id :* id

  (xf :*  yf) . (xg :* yg) = (xf . xg) :* (yf . yg)

 

This all works perfectly fine in Conor's SHE, (as does the thrist example) so I'm wondering where the impedence mismatch comes in and how to gain knowledge of this injectivity to make it work.

 

Also, does it ever make sense for the kind of a kind variable mentioned in a type not to get a functional dependency on the type? 

 

e.g. should

 

class Foo (m :: k -> *)

 

always be

 

class Foo (m :: k -> *) | m -> k

 

?

 

Honest question. I can't come up with a scenario, but you might have one I don't know.

 

-Edward

 

On Fri, Aug 31, 2012 at 5:55 AM, Simon Peyton-Jones <simonpj <at> microsoft.com> wrote:

With the code below, I get this error message with HEAD. And that looks right to me, no?

The current 7.6 branch gives the same message printed less prettily.

 

If I replace the defn of irt with

irt :: a '(i,j) -> Thrist a '(i,j)

irt ax = ax :- Nil

 

then it typechecks.

 

Simon

 

 

Knett.hs:20:10:

    Couldn't match type `x' with '(i0, k0)

      `x' is a rigid type variable bound by

          the type signature for irt :: a x -> Thrist k a x at Knett.hs:19:8

    Expected type: Thrist k a x

      Actual type: Thrist k a '(i0, k0)

    In the expression: ax :- Nil

    In an equation for `irt': irt ax = ax :- Nil

simonpj <at> cam-05-unx:~/tmp$

 

 

{-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures, MultiParamTypeClasses, PolyKinds,

             RankNTypes, TypeOperators, DefaultSignatures, DataKinds,

             FlexibleInstances, UndecidableInstances #-}

 

module Knett where

 

class IMonad (m :: (k -> *) -> k -> *) | m -> k where

  ireturn :: a x -> m a x

 

infixr 5 :-

 

data Thrist :: ((i,i) -> *) -> (i,i) -> * where

  Nil  :: Thrist a '(i,i)

  (:-) :: a '(i,j) -> Thrist a '(j,k) -> Thrist a '(i,k)

 

-- instance IMonad Thrist where

--  ireturn a = a :- Nil

 

irt :: a x -> Thrist a x

irt ax = ax :- Nil

 

 

From: glasgow-haskell-users-bounces <at> haskell.org [mailto:glasgow-haskell-users-bounces <at> haskell.org] On Behalf Of Edward Kmett
Sent: 31 August 2012 03:38
To: glasgow-haskell-users <at> haskell.org
Subject: PolyKind issue in GHC 7.6.1rc1: How to make a kind a functional dependency?

 

If I define the following

 

{-# LANGUAGE FunctionalDependencies, GADTs, KindSignatures, MultiParamTypeClasses, PolyKinds, RankNTypes, TypeOperators, DefaultSignatures, DataKinds, FlexibleInstances, UndecidableInstances #-}

module Indexed.Test where

 

class IMonad (m :: (k -> *) -> k -> *) where 

  ireturn :: a x -> m a x

 

infixr 5 :-

data Thrist :: ((i,i) -> *) -> (i,i) -> * where

  Nil :: Thrist a '(i,i)

  (:-) :: a '(i,j) -> Thrist a '(j,k) -> Thrist a '(i,k)

 

instance IMonad Thrist where

  ireturn a = a :- Nil

 

Then 'ireturn' complains (correctly) that it can't match the k with the kind (i,i). The reason it can't is because when you look at the resulting signature for the MPTC it generates it looks like

 

class IMonad k m where

  ireturn :: a x -> m a x

 

However, there doesn't appear to be a way to say that the kind k should be determined by m. 

 

I tried doing:

 

class IMonad (m :: (k -> *) -> k -> *) | m -> k where 

  ireturn :: a x -> m a x

 

Surprisingly (to me) this compiles and generates the correct constraints for IMonad:

 

ghci> :set -XPolyKinds -XKindSignatures -XFunctionalDependencies -XDataKinds -XGADTs

ghci> class IMonad (m :: (k -> *) -> k -> *) | m -> k where ireturn :: a x -> m a x

ghci> :info IMonad

class IMonad k m | m -> k where

  ireturn :: a x -> m a x

 

But when I add 

 

ghci> :{

Prelude| data Thrist :: ((i,i) -> *) -> (i,i) -> * where

Prelude|   Nil :: Thrist a '(i,i)

Prelude|   (:-) :: a '(i,j) -> Thrist a '(j,k) -> Thrist a '(i,k)

Prelude| :}

 

and attempt to introduce the instance, I crash:

 

ghci> instance IMonad Thrist where ireturn a = a :- Nil

ghc: panic! (the 'impossible' happened)

  (GHC version 7.6.0.20120810 for x86_64-apple-darwin):

    lookupVarEnv_NF: Nothing

 

Please report this as a GHC bug:  http://www.haskell.org/ghc/reportabug

 

Moreover, attempting to compile them in separate modules leads to a different issue. 

 

Within the module, IMonad has a type that includes the kind k and the constraint on it from m. But from the other module, :info shows no such constraint, and the above code again fails to typecheck, but upon trying to recompile, when GHC goes to load the IMonad instance from the core file, it panicks again differently about references to a variable not present in the core.

 

Is there any way to make such a constraint that determines a kind from a type parameter in GHC 7.6 at this time?

 

I tried the Kind hack used in GHC.TypeLits, but it doesn't seem to be applicable to this situation.

 

-Edward

 

_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users <at> haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users

Gmane