Question on simulating dependent types

Learn
#1

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:

  1. Is GHC’s type system powerful enough to write an equivalent version of the Idris code? If so, how can I finish it?
  2. 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.
1 Like
#2

Your code looks fine; you could even inline

MkMsg :: SNat n -> TF n -> TF n

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?

#3

By the way, this is isomorphic to Header -> a -> Msg a.

#4

You seem to have already written the equivalent of the Idris code you showed (more or less). The singleton translation gives

MkMsg :: forall (header :: Header) . SHeader header -> HeaderToType header -> Msg (HeaderToType header)

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.

There’s a bit more information on the GHC wiki (fc · Wiki · Glasgow Haskell Compiler / GHC · GitLab) and a long list of papers about System FC (reading list · Wiki · Glasgow Haskell Compiler / GHC · GitLab). GHC’s implementation still uses System FC more or less as described in the papers, although unfortunately there are many papers about different aspects of the system and not one definitive paper that covers the whole thing. (There is docs/core-spec/core-spec.pdf · master · Glasgow Haskell Compiler / GHC · GitLab which is an excellent reference to System FC as implemented, although it is essentially a list of typing rules that require one to understand the motivation behind them already, and it wouldn’t surprise me if it is out of date in one or two areas.)

4 Likes
#5

I think you forgot the argument to SHeader:

MkMsg :: forall (header :: Header) . SHeader header -> HeaderToType header -> Msg (HeaderToType header)
1 Like
#6

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!

1 Like