[ghc-steering-committee] #364: Unify Nat and Natural, recommendation: accept

[Joachim Breitner]

Hi,

Am Donnerstag, den 01.10.2020, 09:14 -0700 schrieb Iavor Diatchki:
> Joachim, I'd be curious to see an example of the hurdle you run into, if there is a simple example illustrating it.

I wanted to use a datatype (that describes an typed AST) both as values
(where I needed Text or String) and as types (where needed Symbol). I
resorted to a hack like

data FieldName
   = N Symbol -- ^ a properly named field
   | N' T.Text -- ^ Use this in terms (usually not needed)
   | H Nat -- ^ a field hash. Should fit in 32 bit. Also used for tuples 
   | H' Word32 -- ^ Use this in terms (mostly internal)


data SFieldName (n :: FieldName) where
    SN :: KnownSymbol s => Proxy s -> SFieldName ('N s)
    SH :: KnownNat n => Proxy n -> SFieldName ('H n)

fromSFieldName :: SFieldName n -> FieldName
fromSFieldName (SN p) = N' (T.pack (symbolVal p))
fromSFieldName (SH p) = H' (fromIntegral (natVal p))

class Typeable fn => KnownFieldName (fn :: FieldName) where fieldName :: SFieldName fn
instance KnownSymbol s => KnownFieldName ('N s) where
    fieldName = SN (Proxy @s)
instance KnownNat s => KnownFieldName ('H s) where
    fieldName = SH (Proxy @s)

Fullcode at 
https://github.com/nomeata/haskell-candid/blob/2feb0cdbdbfa74f3e4373066b1d5827e5038df9d/src/Codec/Candid/Core.hs#L163-L167

Eventually I just used less type-level computation (and otherwise
greatly restructued that code, so don’t worry too much about helping
here). Maybe using a library like singleton might have made that
easier, or maybe there are tricks that I missed, and I did it all
wrong.


Cheers,
Joachim
-- 
Joachim Breitner
  mail at joachim-breitner.de
  http://www.joachim-breitner.de/