Есть ли удобный способ для построения чисел Пеано большего уровня типа с использованием монопересекающихся?

В монопереходном пакете используются числа Пеано уровня типа для MinLen, Я могу построить их, используя цепочку Succs:

toMinLen [1,2,3] :: Maybe (MinLen (Succ (Succ Zero)) [Int])

но это быстро выходит из-под контроля

toMinLen [1,2,3] :: Maybe (MinLen (Succ (Succ (Succ (Succ (Succ Zero))))) [Int])

Есть ли удобный способ построить большие числа Пеано? Я вижу, что у GHC есть расширение TypeLiterals, но я не уверен, что смогу использовать его здесь. Кроме того, я могу сделать синонимы, такие как:

type One = Succ Zero
type Two = Succ One

и так далее; что-то подобное уже существует где-то?

Источник

3 ответа

Решение

TypeLits отлично подходит для цифр уровня типа. Кроме того, его легко использовать только для синтаксического сахара и оставить базовую специфичную для библиотеки реализацию неизменной.

{-# LANGUAGE
  UndecidableInstances, TypeFamilies,
  DataKinds, TypeOperators #-}

import qualified GHC.TypeLits as TL

data Nat = Zero | Succ Nat

newtype MinLen (n :: Nat) a = MinLen a

Мы должны определить семейство типов, которое преобразует литерал в тип числа:

type family Lit (n :: TL.Nat) :: Nat where
  Lit 0 = Zero
  Lit n = Succ (Lit (n TL.- 1))

Теперь вы можете использовать Lit n всякий раз, когда вам нужно Nat буквальный. В GHCi:

>:kind! MinLen (Lit 3)
MinLen (Lit 3) :: * -> *
= MinLen ('Succ ('Succ ('Succ 'Zero)))
Источник

Для такого рода вещей есть пакет: тип-уровень. Это немного пугающе, и я еще не исследовал это. Но вам не нужно так много энергии, чтобы вы могли бросать свои собственные простые биты.

Если вы готовы использовать UndecidableInstancesвсе довольно просто. Что-то примерно так (я не знаю точно, как натуралы определены в этой библиотеке; если она не использует DataKindsвам, возможно, придется использовать * вид вместо Nat добрый, и вам, возможно, придется написать 'Succ а также 'Zero вместо Succ а также Zero- Я не очень четко понимаю этот аспект)

{-# LANGUAGE UndecidableInstances, TypeFamilies, DataKinds, TypeOperators #-}

module TAR where

-- You wouldn't actually use this line, because the library
-- provides the naturals
data Nat = Zero | Succ Nat

-- Digits and Ten to get things started
type One = Succ Zero
type Two = Succ One
type Three = Succ Two
type Four = Succ Three
type Five = Succ Four
type Six = Succ Five
type Seven = Succ Six
type Eight = Succ Seven
type Nine = Succ Eight
type Ten = Succ Nine

type family Plus (a::Nat) (b::Nat) where
  Plus Zero n = n
  Plus (Succ m) n = Plus m (Succ n)

type family Times (a::Nat) (b::Nat) where
  Times Zero n = Zero
  Times (Succ m) n = Plus n (Times m n)

type Decimal (a::[Nat]) = Decimal' a Zero

type family Decimal' (a::[Nat]) (n::Nat) where
  Decimal' '[] n = n
  Decimal' (a ': bs) n = Decimal' bs (Plus a (Times Ten n))

Тогда вы можете написать что-то вроде

Decimal '[One, Two, Five]

означать 125.

Источник

Вы могли бы портировать type-natural "s QuasiQuoter с.

Источник
Другие вопросы по тегам