Найти следующий фактор KnownNat с учетом начального KnownNat на уровне типа - PullRequest
Новая
       25

Найти следующий фактор KnownNat с учетом начального KnownNat на уровне типа

2 голосов
/ 03 июня 2019

Я работаю над некоторым кодом на Haskell и хочу определить тип, который принимает два KnownNat и приводит к наименьшему коэффициенту второго KnownNat, который больше первого.

ДляНапример, с учетом чисел 13 и 100 результат будет 20, поскольку 20 делит 100 чисто, и между 13 и 20 нет числа, которое делит 100 чисто.Другой пример приводится 96 и 10000 результат будет 100.

Я хотел бы выразить это в Haskell, как-то использовать пакет typelits для его вычисления.,Но я не могу понять, как. 

type a b = ...?

Любая помощь или указатели приветствуются!

1 Ответ

4 голосов
/ 04 июня 2019

Не должно быть слишком сложно. Стандартный алгоритм пробного деления, поднятый до уровня типа, похоже, делает свое дело. 

{-# 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

Попробуйте в ghci: 

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