1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
|
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
module GH55Spec (main, spec) where
import Data.Constraint
import Data.Constraint.Nat
import GHC.TypeLits
import Test.Hspec
newtype GF (n :: Nat) = GF Integer deriving (Eq, Show)
instance KnownNat n => Num (GF n) where
xf@(GF a) + GF b = GF $ (a+b) `mod` (natVal xf)
xf@(GF a) - GF b = GF $ (a-b) `mod` (natVal xf)
xf@(GF a) * GF b = GF $ (a*b) `mod` (natVal xf)
abs = id
signum xf@(GF a) | a==0 = xf
| otherwise = GF 1
fromInteger = GF
x :: GF 5
x = GF 3
y :: GF 5
y = GF 4
foo :: (KnownNat m, KnownNat n) => GF m -> GF n -> GF (Lcm m n)
foo m@(GF a) n@(GF b) = GF $ (a*b) `mod` (lcm (natVal m) (natVal n))
bar :: (KnownNat m) => GF m -> GF m -> GF m
bar (a :: GF m) b = foo a b - foo b a \\ Sub @() (lcmIsIdempotent @m) \\ lcmNat @m @m
z :: GF 5
z = bar x y
spec :: Spec
spec = describe "GH #53" $
it "should normalize Lcm m m" $
z `shouldBe` (GF 0 :: GF (Lcm 5 5))
main :: IO ()
main = hspec spec
|
