type level function with different return kinds
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
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
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@gmail.com
On Sun, 6 Apr 2025, 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’
...
Any ideas how to remove the "same kind" restriction or how to workaround it?
That's the behavior I would expect. Why do you want something different? You could define a type C that has two constructors for A and for B.
On 2025-04-06 00:57, Henning Thielemann wrote:
That's the behavior I would expect. Why do you want something different?
You could define a type C that has two constructors for A and for B. I think you're trying to make a function that either returns constructor for A of type C a, or constructor for B of type C a b
-- () ASCII ribbon campaign - against html e-mail /\ www.asciiribbon.org - against proprietary attachments
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.
Glad you've found your answer :) By the way this is a technique I've used in the package fcf-family: https://hackage.haskell.org/package/fcf-family The idea is that given a Name which uniquely identifies a type family, it should be possible to map it to, well, the type family it names. You will then also need a type family to map to its type, so you get essentially this: type family TypeOf (n :: Name) :: Type type family Eval (n :: Name) :: TypeOf n I've used fcf-family to extend kind-generics to enable Generic instances for data types that involve type families. Cheers, Li-yao On 2025-04-06 2:43 PM, Tom Smeding wrote:
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.
_______________________________________________ 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.
On Sun, Apr 06, 2025 at 12:27:04AM +0200, Zoran Bošnjak wrote:
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.
The way you do this at the type level is with Dynamic: https://www.stackage.org/haddock/lts-23.17/base-4.19.2.0/Data-Dynamic.html#t... Or equivalently, something like data SomeTypeable where MkSomeTypeable :: Typeable a => a -> SomeTypeable So if you can work out how to promote one of those to the kind level then yes. If not then probably no! Tom
participants (7)
-
Brandon Allbery -
D34DB33F -
Henning Thielemann -
Li-yao Xia -
Tom Ellis -
Tom Smeding -
Zoran Bošnjak