Динамически генерировать типы Haskell во время выполнения?

Question

Можно ли определить тип Haskell во время выполнения из данного шаблона? Вот что я имею в виду. Предположим, мне нужен целочисленный тип, который ограничен некоторым диапазоном (неизвестно точно во время компиляции). Я также хочу функцию, которая:

succ 0 = 1 
succ 1 = 2 
... 
succ n = 0 

n неизвестности во время компиляции. Я мог бы сделать что-то вроде этого:

data WrapInt = WrapInt { 
     value  :: Int, 
     boundary :: Int 
} 

wrapInt :: Int -> Int -> WrapInt 
wrapInt boundary value = WrapInt value boundary 

Теперь то, что я хотел бы иметь, чтобы сохранить функцию wrapInt, как это, но, чтобы избежать сохранения границы в качестве значения внутри типа WrapInt. Вместо этого я хотел бы, чтобы он каким-то образом хранился в определении типа, что, конечно же, означает, что тип должен определяться динамически во время выполнения.

Возможно ли достичь этого в Haskell?

Answer 1

Пакет reflection позволяет генерировать новые «локальные» экземпляры класса типов во время выполнения.

Например, предположим, что мы имеем следующие класс типов значений, которые могут «обернуть вокруг»:

{-# LANGUAGE Rank2Types, FlexibleContexts, UndecidableInstances #-} 

import Data.Reflection 
import Data.Proxy 

class Wrappy w where 
    succWrappy :: w -> w 

Определим этот NewType, несущее параметр типа фантом:

data WrapInt s = WrapInt { getValue :: Int } deriving Show 

сделать это номер Wrappy:

instance Reifies s Int => Wrappy (WrapInt s) where 
    succWrappy w@(WrapInt i) = 
     let bound = reflect w 
     in 
     if i == bound 
      then WrapInt 0 
      else WrapInt (succ i) 

часть - это ограничение Reifies s Int. Это означает: «фантомный тип s представляет значение типа Int на уровне типа». Пользователи никогда не определяют экземпляр для Reifies, это делается с помощью внутренней машины reflection.

Так, Reifies s Int => Wrappy (WrapInt s) означает: «всякий раз, когда s представляет значение типа Int, мы можем сделать WrapInt s экземпляр Wrappy».

Функция reflect принимает значение прокси, соответствующее типу фантома, и возвращает фактическое значение Int, которое используется при реализации экземпляра Wrappy.

На самом деле «присвоить» значение к типу фантома, мы используем reify:

-- Auxiliary function to convice the compiler that 
-- the phantom type in WrapInt is the same as the one in the proxy 
likeProxy :: Proxy s -> WrapInt s -> WrapInt s 
likeProxy _ = id 

main :: IO() 
main = print $ reify 5 $ \proxy -> 
    getValue $ succWrappy (likeProxy proxy (WrapInt 5)) 

Обратите внимание, что подпись reify запрещает тип фантомного от выхода из обратного вызова, поэтому мы должны разворачивать результат с getValue.

См. Дополнительные примеры в this Ответьте на, в reflection GitHub repo.

Answer 2

Это не невозможно - просто очень уродливо. Нам понадобятся натуральные числа

data Nat = Z | S Nat 

и ограниченных натуральных числа

data Bounded (n :: Nat) where 
    BZ :: Bounded n 
    BS :: Bounded n -> Bounded (S n) 

Тогда ваша функция должна быть чем-то вроде

succ :: Bounded n -> Bounded n 
succ bn = fromMaybe BZ $ go bn where 
    go :: Bounded n -> Maybe (Bounded n) 
    go = ... 

В go мы должны

1. карты BZ - Nothing, если n - Z (т.е. если Bounded достиг своего максимума и разливалась)
2. карту BZ к Just (BS BZ), если n не Z (то есть, если Bounded не достигла своего максимума).
3. звонок go рекурсивно для случая BS.

Проблема заключается в том, что нет способа получить n на уровне значения. Хаскелл не зависит от этого. Обычным взломом является использование singletons. Запись вручную

data Natty (n :: Nat) where 
    Zy :: Natty Z 
    Sy :: Natty n -> Natty (S n) 

class NATTY (n :: Nat) where 
    natty :: Natty n 

instance NATTY Z where 
    natty = Zy 

instance NATTY n => NATTY (S n) where 
    natty = Sy natty 

Теперь мы можем получить представление стоимости уровня n в Bounded n в go:

succ :: NATTY n => Bounded n -> Bounded n 
succ bn = fromMaybe BZ $ go natty bn where 
    go :: Natty n -> Bounded n -> Maybe (Bounded n) 
    go Zy  BZ  = Nothing 
    go (Sy ny) BZ  = Just (BS BZ) 
    go (Sy ny) (BS bn) = BS <$> go ny bn 

А класс NATTY типа используется для автоматического вывести это значение.

Некоторые тесты:

instance Eq (Bounded n) where 
    BZ == BZ = True 
    BS bn == BS bm = bn == bm 
    _  == _  = False 

zero :: Bounded (S (S Z)) 
zero = BZ 

one :: Bounded (S (S Z)) 
one = BS BZ 

two :: Bounded (S (S Z)) 
two = BS (BS BZ) 

main = do 
    print $ succ zero == zero -- False 
    print $ succ zero == one -- True 
    print $ succ one == two -- True 
    print $ succ two == zero -- True 

code.

---

singletons Используя библиотеку, мы можем определить, как succ

$(singletons [d| data Nat = Z | S Nat deriving (Eq, Show) |]) 

data Bounded n where 
    BZ :: Bounded n 
    BS :: Bounded n -> Bounded (S n) 

succ :: SingI n => Bounded n -> Bounded n 
succ bn = fromMaybe BZ $ go sing bn where 
    go :: Sing n -> Bounded n -> Maybe (Bounded n) 
    go SZ  BZ  = Nothing 
    go (SS ny) BZ  = Just (BS BZ) 
    go (SS ny) (BS bn) = BS <$> go ny bn 

---

Что касается подъема во время выполнения материала на уровне типа, существует два подхода: CPS и existential types.