Git Product home page Git Product logo

finite-typelits's People

Contributors

howtonotwin avatar mniip avatar mstksg avatar raehik avatar turion avatar

Stargazers

avatar avatar avatar avatar avatar avatar avatar

Watchers

avatar avatar avatar avatar avatar

Forkers

mstksg shimuuar howtonotwin sheaf jonascarpay baskaransri raehik turion

finite-typelits's Issues

Generic instance allows to break data abstraction

Generic basically allows unrestricted access to data type constructors. So following example allows us to create Finite with arbitrary content using machinery from fixed-vector-hetero

λ> import Data.Finite
λ> import qualified Data.Vector.HFixed as H
λ> instance H.HVector (Finite n)
λ> H.mk1 666 :: Finite 3
finite 666

fixed-vector-hetero is not necessary. It's just easiest if somewhat roundabout way to create instance of data type using Generic API.

Generic is frequently used to drive serialization instances. Since it doesn't do any checking it allows attack if malicious data is decoded. It's probably better to remove such instance.

Build failure on GHC 8.4.3

finite-typelits-0.1.4.1 fails to build on GHC 8.4.3 with the following error:

Building library for finite-typelits-0.1.4.1..
[1 of 2] Compiling Data.Finite.Internal ( src/Data/Finite/Internal.hs, dist/build/Data/Finite/Internal.o )

src/Data/Finite/Internal.hs:96:10: error:
    • No instance for (GHC.Generics.Generic (Finite n))
        arising from a use of ‘Control.DeepSeq.$dmrnf’
    • In the expression: Control.DeepSeq.$dmrnf @(Finite n)
      In an equation for ‘rnf’: rnf = Control.DeepSeq.$dmrnf @(Finite n)
      In the instance declaration for ‘NFData (Finite n)’
   |
96 | instance NFData (Finite n)
   |          ^^^^^^^^^^^^^^^^^

Loosen constraint from Integer to Num or Integral

Would it be reasonable to suggest that functions that functions that return an Integer be changed so that they return a Num instead? For instance, getFinite :: Finite n -> Integer, could have fromIntegral post-composed, so that it changes to getFinite :: Num o => Finite n -> o.

In the same vein, functions that take an Integer could be changed so that they take an Integral instead by pre-composing toInteger. For instance,

packFinite :: (KnownNat n, Integral o) => o -> Maybe (Finite n)

`quot` isn't modular multiplicative inverse

Please either document that, or re-implement quot (http://hackage.haskell.org/package/integer-gmp-1.0.0.1/docs/GHC-Integer-GMP-Internals.html#v:recipModInteger):

https://en.wikipedia.org/wiki/Modular_multiplicative_inverse

*Data.Finite> map (quot 1) [1,2,3,4] :: [Finite 5]
[finite 1,finite 0,finite 0,finite 0]

vs.

*Data.Fin> let ns = [0,1,2,3,4] in map (quot 1) ns :: [Fin N.Nat5]
[0,1,3,2,4]
*Data.Fin> let ns = [0,1,2,3,4] in zipWith (*) ns (map (quot 1) ns) :: [Fin N.Nat5]
[0,1,1,1,1]

Note: modular inverse works well only for prime modulus.

Perplexing orphan instances

The placement of the Finite type in Data.Finite.Internal, separate from its instances is quite unfortunate. Not only do orphan instances come at a compile-time cost, but older versions of Haddock won't even show them.

Why not simply place everything in Data.Finite.Internal and then reexport only the safe interfaces from Data.Finite?

Inaccurate version bounds / compile error with GHC 7.6

Fyi, this probably just needs a base >= 4.6 bound added to

Configuring component lib from finite-typelits-0.1.1.0
Preprocessing library finite-typelits-0.1.1.0...
[1 of 2] Compiling Data.Finite.Internal ( src/Data/Finite/Internal.hs, /tmp/matrix-worker/1481889125/dist-newstyle/build/x86_64-linux/ghc-7.6.3/finite-typelits-0.1.1.0/build/Data/Finite/Internal.o )

src/Data/Finite/Internal.hs:32:11:
    Not in scope: type constructor or class `KnownNat'

src/Data/Finite/Internal.hs:35:25: Not in scope: `natVal'

src/Data/Finite/Internal.hs:37:102: Not in scope: `natVal'

src/Data/Finite/Internal.hs:44:10:
    Not in scope: type constructor or class `KnownNat'

src/Data/Finite/Internal.hs:47:25: Not in scope: `natVal'

src/Data/Finite/Internal.hs:48:31: Not in scope: `natVal'

src/Data/Finite/Internal.hs:52:25: Not in scope: `natVal'

src/Data/Finite/Internal.hs:56:10:
    Not in scope: type constructor or class `KnownNat'

src/Data/Finite/Internal.hs:66:10:
    Not in scope: type constructor or class `KnownNat'

src/Data/Finite/Internal.hs:67:55: Not in scope: `natVal'

src/Data/Finite/Internal.hs:68:55: Not in scope: `natVal'

src/Data/Finite/Internal.hs:69:55: Not in scope: `natVal'

src/Data/Finite/Internal.hs:74:29: Not in scope: `natVal'

src/Data/Finite/Internal.hs:76:111: Not in scope: `natVal'

src/Data/Finite/Internal.hs:78:10:
    Not in scope: type constructor or class `KnownNat'

src/Data/Finite/Internal.hs:81:10:
    Not in scope: type constructor or class `KnownNat'

Put finite-typelits on stackage

It would be great if finite-typelits could be on stackage, so other projects that depend on it (vector-sized, rhine, ...) can be reenabled there. If you're unsure how that works I'm willing to help and/or maintain.

Finite ordinals are simplices — add the face and degeneracy maps for them!

Simply speaking, a face map is a generalization of shift ≡ face 0 and weaken ≡ face maxBound, and a degeneracy map is its retraction. More information can be found in the usual source.

This implementation seems to work:

face ∷ Finite (size + 1) → Finite size → Finite (size + 1)
face threshold vertex =
  let weakerVertex = weaken vertex
   in if weakerVertex < threshold then weakerVertex else shift vertex

degeneracy ∷ KnownNat size ⇒ Finite (size + 1) → Finite (size + 1) → Finite size
degeneracy threshold vertex = case (strengthen vertex, unshift vertex) of
  (_, Nothing) → 0
  (Nothing, Just smallerVertex) → smallerVertex
  (Just strongerVertex, Just smallerVertex) → if vertex < threshold then strongerVertex else smallerVertex

This is the property that we want to hold: ∀ threshold. degeneracy threshold ∘ face threshold ≡ id. I checked the implementation above with QuickCheck and it seems to hold.

Types of `add` and `multiply` are too loose

The fact that Finite n represents a natural number in the open range [0, n), equivalent to the closed range [0, n − 1] rather than the closed range [0, n], seems to be a consistent source of imprecisions in this library’s types. For example, the current type of add is

add :: Finite n -> Finite m -> Finite (n + m)

but this is too loose, since it implies the result of summing a Finite n value with a Finite m value will produce a value in the range [0, m + n). However, the maximum value is actually (n − 1) + (m − 1), or n + m − 2, which means the type above includes an off-by-one error. The actual type should be

add :: Finite n -> Finite m -> Finite (n + m - 1)

to reflect the actual upper bound.

The situation for multiply is similar, but the differences between the operations make the inaccuracy more drastic than a simple off-by-one error. The current type of multiply is

multiply :: Finite n -> Finite m -> Finite (n * m)

which implies the range of Finite n multiplied by Finite m is [0, n × m), which would be equivalent to the closed range [0, (n × m) − 1]. This is not true, however, since the same reasoning used above reveals that the possible range is actually [0, ((n − 1) × (m − 1)) + 1). This implies that the correct type for multiply should be

multiply :: Finite n -> Finite m -> Finite (((n - 1) * (m - 1)) + 1)

messy as that may be.

finite-typelits doesn't build with ghc 8.6 

[1 of 2] Compiling Data.Finite.Internal ( src/Data/Finite/Internal.hs, dist/build/Data/Finite/Internal.o )
[2 of 2] Compiling Data.Finite      ( src/Data/Finite.hs, dist/build/Data/Finite.o )

src/Data/Finite.hs:150:45: error:
    • Expected kind ‘* -> Nat -> Nat’, but ‘n’ has kind ‘Nat’
    • In the first argument of ‘Finite’, namely ‘(n * m)’
      In the type signature:
        multiply :: Finite n -> Finite m -> Finite (n * m)
    |
150 | multiply :: Finite n -> Finite m -> Finite (n * m)
    |                                             ^^^^^

src/Data/Finite.hs:162:65: error:
    • Expected kind ‘* -> Nat -> Nat’, but ‘n’ has kind ‘Nat’
    • In the first argument of ‘Finite’, namely ‘(n * m)’
      In the type signature:
        combineProduct :: KnownNat n =>
                          (Finite n, Finite m) -> Finite (n * m)
    |
162 | combineProduct :: KnownNat n => (Finite n, Finite m) -> Finite (n * m)
    |                                                                 ^^^^^

src/Data/Finite.hs:174:42: error:
    • Expected kind ‘* -> Nat -> Nat’, but ‘n’ has kind ‘Nat’
    • In the first argument of ‘Finite’, namely ‘(n * m)’
      In the type signature:
        separateProduct :: KnownNat n =>
                           Finite (n * m) -> (Finite n, Finite m)
    |
174 | separateProduct :: KnownNat n => Finite (n * m) -> (Finite n, Finite m)
    |                                          ^^^^^

Recommend Projects

  • React photo React

    A declarative, efficient, and flexible JavaScript library for building user interfaces.

  • Vue.js photo Vue.js

    🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.

  • Typescript photo Typescript

    TypeScript is a superset of JavaScript that compiles to clean JavaScript output.

  • TensorFlow photo TensorFlow

    An Open Source Machine Learning Framework for Everyone

  • Django photo Django

    The Web framework for perfectionists with deadlines.

  • D3 photo D3

    Bring data to life with SVG, Canvas and HTML. 📊📈🎉

Recommend Topics

  • javascript

    JavaScript (JS) is a lightweight interpreted programming language with first-class functions.

  • web

    Some thing interesting about web. New door for the world.

  • server

    A server is a program made to process requests and deliver data to clients.

  • Machine learning

    Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.

  • Game

    Some thing interesting about game, make everyone happy.

Recommend Org

  • Facebook photo Facebook

    We are working to build community through open source technology. NB: members must have two-factor auth.

  • Microsoft photo Microsoft

    Open source projects and samples from Microsoft.

  • Google photo Google

    Google ❤️ Open Source for everyone.

  • D3 photo D3

    Data-Driven Documents codes.