[Haskell-cafe] Limitations of generalization of type constructors
Tom Ellis
tom-lists-haskell-cafe-2023 at jaguarpaw.co.uk
Mon Sep 18 09:55:38 UTC 2023
Hello Cafe,
Generalization of types in type constructors behaves strangely
compared to the same behaviour at the term level. I was wondering
whether this is expected, whether it's a known issue that's due to be
resolved, or is a known issue that can't be resolved for some
technical reason.
This mail is a literate Haskell file.
> {-# LANGUAGE DataKinds #-}
> {-# LANGUAGE PolyKinds #-}
> {-# LANGUAGE RankNTypes #-}
> {-# LANGUAGE StandaloneKindSignatures #-}
> {-# LANGUAGE TypeFamilies #-}
>
> {-# OPTIONS_GHC -Wall #-}
> {-# OPTIONS_GHC -Wno-unticked-promoted-constructors #-}
>
> import Prelude hiding (const)
> import Data.Kind (Type)
`f` takes an argument of polymorphic type
> f :: (forall (z :: Type). Maybe z -> Int) -> Int
> f k = k (Just True)
`c1` is an argument that will fit there. Its type matches exactly.
> c1 :: forall (z :: Type). Maybe z -> Int
> c1 _ = 0
>
> fc1 :: Int
> fc1 = f c1
`c2` will fit there but its type doesn't match exactly. `z` will have
to be substituted with `Maybe z`, obtaining the type
forall (z :: Type). Maybe z -> Int
which does fit exactly.
> c2 :: forall (z :: Type). z -> Int
> c2 _ = 0
>
> fc2 :: Int
> fc2 = f c2
`const` will fit there, once `z` is substituted with `Maybe z`, the
`Int` argument applied and the quantifer moved, obtaining the type
forall (z :: Type). Maybe z -> Int
which does fit exactly.
> const :: forall (z :: Type). Int -> z -> Int
> const x _ = x
>
> fc3 :: Int
> fc3 = f (const 0)
The story for type constructors is not so pleasant. I can define an
analogue of `f` on the type level:
> type F :: (forall (z :: Type). Maybe z -> Type) -> Type
> newtype F k = F (k (Just Bool))
and the analogue of `c1` fits exactly:
> type C1 :: forall (z :: Type). Maybe z -> Type
> data C1 m = C1
>
> type FC1 :: Type
> type FC1 = F C1
but the analogue of `c2` does not:
> type C2 :: forall (z :: Type). z -> Type
> data C2 m = C2
>
> -- Occurs check: cannot construct the infinite kind: z ~ Maybe z
> -- type FC2 :: Type
> -- type FC2 = F C2
nor does the analogue of `const`:
> type Const :: forall (z :: Type). Type -> Maybe z -> Type
> newtype Const z a = Const z
>
> -- • Expected kind ‘forall z. Maybe z -> *’,
> -- but ‘Const ()’ has kind ‘Maybe a0 -> *’
> -- type FC3 :: Type
> -- type FC3 = F (Const ())
To get the analogue of `const` we have to be much more specific:
> type OtherConst :: Type -> forall (z :: Type). Maybe z -> Type
> newtype OtherConst z b = OtherConst z
>
> type FC4 :: Type
> type FC4 = F (OtherConst ())
This is rather unfortunate because it limits generic programming at
the type level!
More information about the Haskell-Cafe
mailing list