search

clash-lang / ghc-typelits-natnormalise

Normalise GHC.TypeLits.Nat equations
Other
43 stars 15 forks source link

(KnownNat n) should entail (KnownNat (96 * n)) #8

Closed ggreif closed 8 years ago

ggreif commented 8 years ago

Consider this snippet (randomly taken from some CLaSH code):

-- Index into a chunked vector
(!!!) :: (KnownNat n, KnownNat (n * 96)) => Vec n (Vec 96 a) -> Index (n * 96) -> a
vec !!! indx = let (sl, chan) = indx `quotRem` 96 in vec !! sl !! chan

The KnownNat (n * 96) constraint should not be necessary when NatNormalise is available, as it can be derived from KnownNat n.

christiaanb commented 8 years ago

Yes it should... but I don't see particularly what this has to do with normalisation of expressions.

Given that type-checker plugins can destroy type-safety, I prefer to keep the functionality of plugins contained. So perhaps this functionality should be put into another plugin.

christiaanb commented 8 years ago

Additionally, I have no clue how to do this with the GHC API. https://downloads.haskell.org/~ghc/7.10.3/docs/html/libraries/ghc-7.10.3/TcEvidence.html#t:EvTerm lists the constructors for evidence, and although it allows us to create a KnownNat dictionary from an Integer using EvLit, it does now allow arbitrary Core expressions as evidence. We would need the arbitrary Core expressions so we can apply *96 to the KnownNat n dictionary to create the KnownNat (n*96) dictionary. See also: https://ghc.haskell.org/trac/ghc/wiki/Plugins/TypeChecker#Underdiscussion:EmbeddingCoreExprinEvTerm

christiaanb commented 8 years ago

It could also be done manually:

{-# LANGUAGE ScopedTypeVariables #-}

(!!!) :: forall n a . (KnownNat n) => Vec n (Vec 96 a) -> Index (n * 96) -> a
vec !!! indx = case mulSNat (snat :: SNat n) d96 of
  SNat _ -> let (sl, chan) = indx `quotRem` 96 in vec !! sl !! chan

In CLaSH 1.0 (based on GHC8), this will become:

{-# LANGUAGE ScopedTypeVariables, TypeApplications #-}

(!!!) :: forall n a . (KnownNat n) => Vec n (Vec 96 a) -> Index (n * 96) -> a
vec !!! indx = case mulSNat (SNat @n) d96 of
  SNat -> let (sl, chan) = indx `quotRem` 96 in vec !! sl !! chan
christiaanb commented 8 years ago

I stand corrected, this can be done, because I just did it. I'll release the plugin soon and I'll write a blog post.

christiaanb commented 8 years ago

https://github.com/clash-lang/ghc-typelits-knownnat

christiaanb commented 8 years ago

GHC 8.0.1+ only though