[Haskell-cafe] type level function with different return kinds

[Tom Smeding]

I played around a little, and it seems that GHC has some support for 
dependent quantification here:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
module M where

import GHC.TypeLits

data A = A1 | A2
data B = B1 | B2

type family K (n :: Nat) where
   K 0 = A
   K 1 = A
   K 2 = B
   K 3 = B

type F :: forall (n :: Nat) -> K n
type family F n where
      F 0 = 'A1
      F 1 = 'A2
      F 2 = 'B1
      F 3 = 'B2

I put it online in a playground paste here: 
https://play.haskell.org/saved/Pcx912j0

It typechecks, but I didn't test if it indeed works in practice.

On 06-04-2025 00:27, Zoran Bošnjak wrote:
> Dear haskellers,
> is it possible to write a type/kind level function that returns types 
> of different kinds for different inputs. Either by using open/closed 
> type families, a typeclass, extensions or any other type level magic. 
> Something like this:
>
> {-# LANGUAGE DataKinds #-}
> {-# LANGUAGE TypeFamilies #-}
>
> import GHC.TypeLits
>
> data A = A1 | A2
> data B = B1 | B2
>
> type family F (n :: Nat) where
>     F 0 = 'A1
>     F 1 = 'A2
>     F 2 = 'B1
>     F 3 = 'B2
>
> The problem with this approach is that (F 0) and (F 1) are ok, but not 
> in combination with (F 2). The error says:
>     • Expected kind ‘A’, but ‘'B1’ has kind ‘B’
>
> If I instead write:
> type family F (n :: Nat) :: k where
> ... I get compile error already on the (F 0) line
>     • Expected kind ‘k’, but ‘'A1’ has kind ‘A’
>
> Any ideas how to remove the "same kind" restriction or how to 
> workaround it?
>
> I am using ghc 9.6.6.
>
> regards,
> Zoran
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.