fI am learning singletons package these days and have encountered some difficulties. I would like to translate the following Idris code into Haskell but failed:
data Header : Type where
MkHeader : (ver : Int) -> (val : Int) -> Header
headerToType : Header -> Type
headerToType (MkHeader ver val) = case ver of
1 => Int
2 => String
_ => ()
data Msg : Type -> Type where
MkMsg : (header : Header)
-> (body : headerToType header)
-> Msg (headerToType header)
I know that I can use type families to write a “function” on types and get the runtime witness of a singleton type. But I still can not finish it:
data Header = Header
{ headerVer :: Int
, headerVal :: Int
}
type family TF (n :: Nat) where
TF 0 = Int
TF 1 = String
TF a = ()
data Msg a where
MkMsg :: (a ~ TF n) => SNat n -> a -> Msg a -- should we add the constraint here?
{-
realMkMsg :: Header -> a -> Msg a -- or (forall a. a -> Msg a) ?
realMkMsg h = withSomeSing (fromIntegral (headerVer h))
(\sn payload -> MkMsg sn payload) -- error, 'a' is a rigid type var!
-}
So my questions are:
Is GHC’s type system powerful enough to write an equivalent version of the Idris code? If so, how can I finish it?
What is the exact strength of GHC’s type system? I have heard that it is System F plus coercions. Does it fit the actual GHC implementation nowadays well? I also would like to know the meaning of “coercions” and its contribution to the whole type system.
But to finish your code, yes your original code didnt work because your type of realMkMsg :: Header -> a -> Msg a claims that the user can choose any type a and any Header value and get back a Msg a, but you want the type a to be constrained based on the Header. So yes, you’d want
realMkMsg :: Header -> (forall a. a -> Msg a)
Although I’m not sure if that would work (do you have ImpredicativeTypes enabled?). You might need another GADT
data SomeMkMsg = forall a. SomeMkMsg (a -> Msg a)
and do
realMkMsg :: Header -> SomeMkMsg
But I’m not sure how youd use it; how would the caller inspect what type is required to pass in?
I’m not sure what you are trying to do with realMkMsg, but the issue you run into is that if you have only a runtime Header argument (and not also a SHeader header singleton) then the argument isn’t known statically. Thus you would need to use an existential type (encoded either using a data constructor like SomeMkMsg, or a higher-rank type) to work with the statically-unknown value.
Is there more Idris code you are trying to translate? In general one can get fairly far with the singleton encoding, but it becomes increasingly clunky as one tries to translate more complex dependently-typed code, because of the limits on which Haskell expressions can be translated to types.
System FC is basically System F plus higher kinds (aka System Fω excluding type lambda), algebraic data types and coercions. Coercions are equality proofs between types, used in the translation of newtypes, GADTs and type families.
Thank you for your detailed reply! I have finally realized that Msg is a dependent pair (Sigma-type). So the equivalent code is
data Msg a where
MkMsg :: (TF n ~ a) => SNat n -> a -> Msg a
data SigmaMsg where
MkSigmaMsg :: forall (n :: Nat). SNat n -> TF n -> SigmaMsg
withSigmaMsg :: SigmaMsg -> (forall (n :: Nat) => SNat n -> TF n -> r)) -> r
withSigmaMsg (MkSigmaMsg sn x) f = f sn x
toSigmaMsg :: Msg a -> SigmaMsg
toSigmaMsg (MkMsg sn x) = MkSigmaMsg sn x
fromSigmaMsg :: forall (a :: Nat). (KnownNat a) => SigmaMsg -> Maybe (TF a)
fromSigmaMsg (MkSigmaMsg sn x) = case sn %~ (sing :: SNat a) of
Proved Refl -> Just x
Disproved _ -> Nothing
Now I can write Sigma and Pi type using these tricks… I will refer to the listed papers for more detailed understand… Thanks!