Skip to content

Instantly share code, notes, and snippets.

@glaebhoerl
Forked from nfrisby/GHC_Query
Created Oct 6, 2012
Embed
What would you like to do?
Exploring kind-indexed type constraints in GHC 7.6
{-# LANGUAGE PolyKinds, GADTs, DataKinds, TypeFamilies, TypeOperators,
MultiParamTypeClasses, FlexibleContexts, FlexibleInstances,
UndecidableInstances #-}
module GHC_Query where
data Proxy (t :: k) = Proxy
data KindProxy (t :: *) = KindProxy -- a type-level proxy for kinds
data Nat = Z | S Nat
-- count the number of type arguments that the kind specifies
type family CountArgs (kp :: KindProxy k) :: Nat
type instance CountArgs (kp :: KindProxy *) = Z
type instance CountArgs (kp :: KindProxy (kD -> kR))
= S (CountArgs ('KindProxy :: KindProxy kR))
class NUnits (n :: Nat) where type Ts n :: [k]
instance NUnits Z where type Ts Z = '[]
instance NUnits n => NUnits (S n) where type Ts (S n) = () ': Ts n
-- a handle to test the behavior of NUnits
demonstrate_NUnits :: (n ~ CountArgs ('KindProxy :: KindProxy k), NUnits n) =>
Proxy (t :: k) -> Proxy (Ts n :: [*])
demonstrate_NUnits _ = Proxy
data GADT :: [*] -> * where
GZ :: GADT '[]
GS :: GADT ts -> GADT (() ': ts)
class CLASS (t :: k) where
method :: (n ~ CountArgs ('KindProxy :: KindProxy k), NUnits n) => Proxy t -> GADT (Ts n)
-- this compiles now
instance CLASS (t :: *) where method _ = GZ
-- testing in GHCi
{-
*GHC_Query> :i demonstrate_NUnits
demonstrate_NUnits ::
(n ~ CountArgs k ('KindProxy k), NUnits n) =>
Proxy k t -> Proxy [*] (Ts * n)
-- Defined at frisby.hs:31:1
-- I think :i just regurgitates the signature from the source file?
*GHC_Query> :t demonstrate_NUnits
demonstrate_NUnits
:: NUnits (CountArgs * ('KindProxy *)) =>
Proxy * t -> Proxy [*] (Ts * (CountArgs * ('KindProxy *)))
-- Uses * instead of k as before, substitutes in our 'n' tyvar, doesn't simplify the output type (as before)
*GHC_Query> :set -XPolyKinds -XDataKinds
*GHC_Query> :t demonstrate_NUnits
demonstrate_NUnits
:: NUnits (CountArgs k ('KindProxy k)) =>
Proxy k t -> Proxy [*] (Ts * (CountArgs k ('KindProxy k)))
-- Now it's using k
*GHC_Query> :t demonstrate_NUnits (Proxy :: Proxy Int)
demonstrate_NUnits (Proxy :: Proxy Int) :: Proxy [*] (Ts * 'Z)
*GHC_Query> :t demonstrate_NUnits (Proxy :: Proxy Maybe)
demonstrate_NUnits (Proxy :: Proxy Maybe)
:: Proxy [*] (Ts * ('S 'Z))
*GHC_Query> :t demonstrate_NUnits (Proxy :: Proxy (,))
demonstrate_NUnits (Proxy :: Proxy (,))
:: Proxy [*] (Ts * ('S ('S 'Z)))
-- It's still not simplifying the output type, but this might be just a for-display thing
-- Wasn't there a version of :t added at some point which simplified away type functions? :t! or :k! or something? neither of those were recognized when I tried them
-- anyway, using the usual workaround...
*GHC_Query> show $ demonstrate_NUnits (Proxy :: Proxy Int)
<interactive>:9:1:
No instance for (Show (Proxy [*] ('[] *)))
arising from a use of `show'
Possible fix:
add an instance declaration for (Show (Proxy [*] ('[] *)))
In the expression: show
In the expression: show $ demonstrate_NUnits (Proxy :: Proxy Int)
In an equation for `it':
it = show $ demonstrate_NUnits (Proxy :: Proxy Int)
-- Now we see that it does get the correct type
*GHC_Query> show $ demonstrate_NUnits (Proxy :: Proxy Maybe)
<interactive>:10:1:
No instance for (Show (Proxy [*] ((':) * () ('[] *))))
arising from a use of `show'
Possible fix:
add an instance declaration for
(Show (Proxy [*] ((':) * () ('[] *))))
In the expression: show
In the expression: show $ demonstrate_NUnits (Proxy :: Proxy Maybe)
In an equation for `it':
it = show $ demonstrate_NUnits (Proxy :: Proxy Maybe)
-- Also the correct type
*GHC_Query> show $ demonstrate_NUnits (Proxy :: Proxy (,))
<interactive>:11:1:
No instance for (Show (Proxy [*] ((':) * () ((':) * () ('[] *)))))
arising from a use of `show'
Possible fix:
add an instance declaration for
(Show (Proxy [*] ((':) * () ((':) * () ('[] *)))))
In the expression: show
In the expression: show $ demonstrate_NUnits (Proxy :: Proxy (,))
In an equation for `it':
it = show $ demonstrate_NUnits (Proxy :: Proxy (,))
-- Also the correct type
-- Let's try something else
*GHC_Query> let foo :: Proxy '[]; foo = demonstrate_NUnits (Proxy :: Proxy Int)
<interactive>:12:29:
Couldn't match kind `k' with `*'
`k' is a rigid type variable bound by
the type signature for foo :: Proxy [k] ('[] k)
at <interactive>:12:12
Expected type: Proxy [k] ('[] k)
Actual type: Proxy [*] (Ts * 'Z)
In the return type of a call of `demonstrate_NUnits'
In the expression: demonstrate_NUnits (Proxy :: Proxy Int)
In an equation for `foo':
foo = demonstrate_NUnits (Proxy :: Proxy Int)
-- Hmm, that's not right... but it works if we add a kind signature:
*GHC_Query> let foo :: Proxy ('[] :: [*]); foo = demonstrate_NUnits (Proxy :: Proxy Int)
-- And higher kinds also work:
*GHC_Query> let foo :: Proxy '[()]; foo = demonstrate_NUnits (Proxy :: Proxy Maybe)
*GHC_Query> let foo :: Proxy '[(), ()]; foo = demonstrate_NUnits (Proxy :: Proxy (,))
-}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment