CODEWITHSUNDEEP
haskelltype-level-computation
user2882307
user2882307

Reputation:

Find next factor of KnownNat given a starting KnownNat at type level

I'm working on some Haskell code and I want to define a type that takes two KnownNat and results in the smallest factor of the second KnownNat that is greater then the first.

For instance given the numbers 13 and 100 the result would be 20 since 20 divides 100 cleanly and there is no number between 13 and 20 that divides 100 cleanly. Another example is given 96 and 10000 the result would be 100.

The way I wanted to express this in Haskell is to somehow use the typelits package to compute it. But I can't really figure out how.

type a b = ...?

Any help or pointers are appreciated!

Upvotes: 1

Views: 85

Answers (1)

Daniel Wagner
Daniel Wagner

Reputation: 152837

Shouldn't be too hard. The standard trial-division algorithm, lifted to the type level, seems to do the trick.

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
import GHC.TypeLits

type FactorGT a b = FactorGTRaw a b (CmpNat (Mod b a) 0)

type family FactorGTRaw a b v where
    FactorGTRaw a b EQ = a
    FactorGTRaw a b _ = FactorGT (a+1) b

Try it out in ghci:

> :k! FactorGT 13 100
FactorGT 13 100 :: Nat
= 20
> :k! FactorGT 96 1000
FactorGT 96 1000 :: Nat
= 100

Upvotes: 2

Related Questions