Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Closed
ggreif opened this issue Aug 4, 2016 · 6 comments
Closed

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

ggreif opened this issue Aug 4, 2016 · 6 comments

Comments

@ggreif
Copy link
Contributor

@ggreif ggreif commented Aug 4, 2016

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
Copy link
Contributor

@christiaanb christiaanb commented Aug 4, 2016

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
Copy link
Contributor

@christiaanb christiaanb commented Aug 4, 2016

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
Copy link
Contributor

@christiaanb christiaanb commented Aug 4, 2016

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
Copy link
Contributor

@christiaanb christiaanb commented Aug 10, 2016

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
Copy link
Contributor

@christiaanb christiaanb commented Aug 10, 2016

GHC 8.0.1+ only though

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Linked pull requests

Successfully merging a pull request may close this issue.

None yet
2 participants
You can’t perform that action at this time.