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

[Brandon Allbery]

I wouldn't expect that to work any more than I would expect a normal
function to be able to produce Int or String on demand, absent dependent
types.

On Sat, Apr 5, 2025 at 6:51 PM Zoran Bošnjak <zoran.bosnjak at via.si> 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.



-- 
brandon s allbery kf8nh
allbery.b at gmail.com
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20250405/237b7c25/attachment.html>