[Haskell-cafe] Rank N Kinds

Roman Cheplyaka roma at ro-che.info
Wed Jul 31 21:45:10 CEST 2013


That's because types that belong to most non-star kinds cannot have
values.

  data Foo (a :: k) = Foo

is okay,

  data Foo (a :: k) = Foo a

is bad because there cannot be a field of type a :: k.

So no, no useful examples exist, because you wouldn't be able to use
such a data constructor even if you could declare it.

Roman

* Wvv <vitea3v at rambler.ru> [2013-07-31 11:40:17-0700]
> OMG!
> I still have 7.6.3. It has old Typeable.
> 
> I misunderstood PolyKinds a bit. It looks like k /= **, k ~ *******...
> 
> But we cannot use "CloseKinds" like
> 
> data Foo (a::k) = Foo a -- catch an error "Expected kind `OpenKind', but `a' has
> kind `k'"
> 
> 
> with RankNKinds we could write:
> data Foo (a::**) = Foo a
> data Bar (a::***) = Bar a
> 
> So, now the task is more easy:
> I'm asking for useful examples with "CloseKinds" with ** and higher, and any
> useful examples for *** and higher
> 
> cheers, Wvv
> 
> 29 Jul 2013 at 14:44:50, José Pedro Magalhães [via Haskell]
> (ml-node+s1045720n5733561h30 at n5.nabble.com) wrote:
> 
>   Hi,
> 
>   On Fri, Jul 26, 2013 at 10:42 PM, Wvv <[hidden email]> wrote:
> 
>     First useful use is in Typeable.
>     In GHC 7.8
>     class Typeable (a::k) where ... <<==>> class Typeable (a ::**) where ...
> 
>     But we can't write
>     data Foo (a::k)->(a::k)->* ... deriving Typeable
> 
> 
>   Why not? This works fine in 7.7, as far as I know.
> 
> 
>   Cheers,
>   Pedro
> 
> 
> 
> 
> --
> View this message in context: http://haskell.1045720.n5.nabble.com/Rank-N-Kinds-tp5733482p5733667.html
> Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.

> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe





More information about the Haskell-Cafe mailing list