Вероятно, можно утверждать, что TH более уместен в подобных случаях.Тем не менее, я все равно сделаю это с типами.
Проблема здесь в том, что все слишком дискретно .Вы не можете перебрать префиксы, чтобы найти правильный, и вы не выражаете транзитивность желаемого порядка.Мы можем решить это любым путем.
Для рекурсивного решения мы сначала создаем натуральные числа и логические значения на уровне типа:
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeFamilies #-}
data No = No deriving (Show)
data Yes = Yes deriving (Show)
newtype S nat = Succ nat deriving (Show)
data Z = Zero deriving (Show)
type Zero = Z
type One = S Zero
type Two = S One
type Three = S Two
Немного простой арифметики:
type family Plus x y :: *
type instance Plus x Z = x
type instance Plus Z y = y
type instance Plus (S x) (S y) = S (S (Plus x y))
type family Times x y :: *
type instance Times x Z = Z
type instance Times x (S y) = Plus x (Times y x)
Предикат "меньше или равно" и простая условная функция:
type family IsLTE n m :: *
type instance IsLTE Z Z = Yes
type instance IsLTE (S m) Z = No
type instance IsLTE Z (S n) = Yes
type instance IsLTE (S m) (S n) = IsLTE m n
type family IfThenElse b t e :: *
type instance IfThenElse Yes t e = t
type instance IfThenElse No t e = e
И преобразования из префиксов SI в величину, которую они представляют:
type family Magnitude si :: *
type instance Magnitude Kilo = Three
type instance Magnitude Mega = Three `Times` Two
type instance Magnitude Giga = Three `Times` Three
... и т. Д.
Теперь, чтобы найти меньший префикс, вы можете сделать это:
type family Smaller x y :: *
type instance Smaller x y = IfThenElse (Magnitude x `IsLTE` Magnitude y) x y
Учитывая, что все здесь имеет взаимно однозначное соответствие между типоми единственный нулевой конструктор, населяющий его, это можно перевести на уровень термина, используя общий класс, подобный этому:
class TermProxy t where term :: t
instance TermProxy No where term = No
instance TermProxy Yes where term = Yes
{- More instances here... -}
smaller :: (TermProxy a, TermProxy b) => a -> b -> Smaller a b
smaller _ _ = term
Заполнение деталей по мере необходимости.
ДругойПодход включает использование функциональных зависимостей и перекрывающихся экземпляров для написания универсального экземпляра для заполнения пробелов - чтобы вы могли написать конкретные экземпляры для Kilo
Это углубляется в трактовку функциональных зависимостей как того, что они есть - языка программирования примитивной логики.Если вы когда-либо использовали Пролог, у вас должна быть грубая идея.В некотором смысле это хорошо, потому что вы можете позволить компилятору разобраться, основываясь на более декларативном подходе.С другой стороны, это также ужасно, потому что ...
- Экземпляры выбираются без учета ограничений, только заголовок экземпляра.
- Нет пути назад для поиска решения.
- Чтобы выразить подобные вещи, вы должны включить
UndecidableInstances из-за очень консервативных правил GHC о том, что, как он знает, прекратится;но тогда вы должны позаботиться о том, чтобы средство проверки типов не отправлялось в бесконечный цикл.Например, было бы очень легко сделать это случайно, учитывая такие экземпляры, как Smaller Kilo Kilo Kilo и что-то вроде (Smaller a s c, Smaller t b s) => Smaller a b c - подумайте, почему.
Fundeps и перекрывающиеся экземпляры строго более мощные, чем typeсемейства, но они неуклюжи в использовании в целом и чувствуют себя несколько неуместно по сравнению с более функциональным, рекурсивным стилем, который использует последний.
О, и для полноты, вот третий подход: На этот раз мы злоупотребляем дополнительными возможностями, которые дают нам перекрывающиеся экземпляры, чтобы напрямую реализовать рекурсивное решение, а не путем преобразования в натуральные числа и использования структурной рекурсии.
Во-первых, измените желаемый порядок как тип.-уровневый список:
data MIN = MIN deriving (Show)
data MAX = MAX deriving (Show)
infixr 0 :<
data a :< b = a :< b deriving (Show)
siPrefixOrd :: MIN :< Kilo :< Mega :< Giga :< Tera :< MAX
siPrefixOrd = MIN :< Kilo :< Mega :< Giga :< Tera :< MAX
Реализация предиката равенства для типов с использованием некоторых перекрывающихся махинаций:
class (TypeEq' () x y b) => TypeEq x y b where typeEq :: x -> y -> b
instance (TypeEq' () x y b) => TypeEq x y b where typeEq _ _ = term
class (TermProxy b) => TypeEq' q x y b | q x y -> b
instance (b ~ Yes) => TypeEq' () x x b
instance (b ~ No) => TypeEq' q x y b
Альтернативный класс "меньше чем", сдва простых случая:
class IsLTE a b o r | a b o -> r where
isLTE :: a -> b -> o -> r
instance (IsLTE a b o r) => IsLTE a b (MIN :< o) r where
isLTE a b (_ :< o) = isLTE a b o
instance (No ~ r) => IsLTE a b MAX r where
isLTE _ _ MAX = No
И затем рекурсивный случай со вспомогательным классом, используемым для отсрочки рекурсивного шагана основе анализа случая логического типа уровня:
instance ( TypeEq a x isA, TypeEq b x isB
, IsLTE' a b isA isB o r
) => IsLTE a b (x :< o) r where
isLTE a b (x :< o) = isLTE' a b (typeEq a x) (typeEq b x) o
class IsLTE' a b isA isB xs r | a b isA isB xs -> r where
isLTE' :: a -> b -> isA -> isB -> xs -> r
instance (Yes ~ r) => IsLTE' a b Yes Yes xs r where isLTE' a b _ _ _ = Yes
instance (Yes ~ r) => IsLTE' a b Yes No xs r where isLTE' a b _ _ _ = Yes
instance (No ~ r) => IsLTE' a b No Yes xs r where isLTE' a b _ _ _ = No
instance (IsLTE a b xs r) => IsLTE' a b No No xs r where
isLTE' a b _ _ xs = isLTE a b xs
По сути, это берет список уровня типа и два произвольных типа, затем идет по списку и возвращает Yes, если он находит первыйвведите, или No, если он найдет второй тип или достигнет конца списка.
Это на самом деле своего рода ошибка (вы можете понять, почему, если вы думаете о том, что происходит, если один или оба типа не отображаются ')в списке), а также склонен к сбою - прямая рекурсия, подобная этой, использует стек сокращения контекста в GHC, который очень мелок, поэтому его легко исчерпать и получить переполнение стека на уровне типов (ха-ха, да,шутка пишет сама) вместо того ответа, который вы хотели.