История изменений
Исправление qnikst, (текущая версия) :
> guessProof :: (KnownNat n, n <= 255) => SomeNat -> Proxy n -> Maybe (Proof2D LessThen255D)
> guessProof (SomeNat p) n = case sameNat p n of
> Just _ -> Just $ Proof2D (c2dk n) LessThen255D n
> Nothing -> Nothing
> type family Guesses (n::Nat) :: [Nat] where
> Guesses 0 = '[0]
> Guesses n = n ': Guesses (n-1)
> g :: Proxy n -> Proxy (Guesses n)
> g _ = Proxy
> class GuessProof (n :: [Nat]) where
> proof :: SomeNat -> Proxy n -> Maybe (Proof2D LessThen255D)
> instance GuessProof '[] where
> proof _ _ = Nothing
> instance (KnownNat n, n <= 255) => GuessProof (n ': ns) where
> proof s p = guessProof s (inner p)
> where inner :: Proxy (n ': ns) -> Proxy (n::Nat)
> inner _ = Proxy
оно даже работает с горем пополам, но блин проще использовать свои числа, чем Num.
P.S. естественно в реальном коде это нафиг не надо.
Исходная версия qnikst, :
> guessProof :: (KnownNat n, n <= 255) => SomeNat -> Proxy n -> Maybe (Proof2D LessThen255D)
> guessProof (SomeNat p) n = case sameNat p n of
> Just _ -> Just $ Proof2D (c2dk n) LessThen255D n
> Nothing -> Nothing
> data N = Z | S N
> type family Guesses (n::Nat) :: [Nat] where
> Guesses 0 = '[0]
> Guesses n = n ': Guesses (n-1)
> g :: Proxy n -> Proxy (Guesses n)
> g _ = Proxy
> class GuessProof (n :: [Nat]) where
> proof :: SomeNat -> Proxy n -> Maybe (Proof2D LessThen255D)
> instance GuessProof '[] where
> proof _ _ = Nothing
> instance (KnownNat n, n <= 255) => GuessProof (n ': ns) where
> proof s p = guessProof s (inner p)
> where inner :: Proxy (n ': ns) -> Proxy (n::Nat)
> inner _ = Proxy
оно даже работает с горем пополам, но блин проще использовать свои числа, чем Num.