Нормализующие неравенства TypeNats - PullRequest
Новая
       31

Нормализующие неравенства TypeNats

2 голосов
/ 30 марта 2019

У меня есть две функции, обе с типом Nat (из TypeNats), у обеих есть оператор типа сравнения <=.Ограничение 2 <= n для функции b содержит ограничение 1 <= n для функции a.Есть ли способ заставить ghc решить, что 2 <= n удовлетворяет ограничению 1 <= n, поэтому мне не нужно указывать оба ограничения (1 <= n, 2 <= n) для b?

Приведенный ниже код демонстрирует ошибку.

{-# LANGUAGE KindSignatures, TypeOperators, ScopedTypeVariables, 
             DataKinds, TypeFamilies #-}

import GHC.TypeNats
import Data.Proxy

a :: forall (a :: Nat). 1 <= a => Proxy a -> Int
a = undefined

b :: forall (a :: Nat). 2 <= a => Proxy a -> Int
b = a

Приводит к ошибке компиляции 

• Could not deduce: (1 <=? a) ~ 'True arising from a use of ‘a’
  from the context: 2 <= a
    bound by the type signature for:
               b :: forall (a :: Nat). (2 <= a) => Proxy a -> Int
    at Example.hs:9:1-48
• In the expression: a
  In an equation for ‘b’: b = a
• Relevant bindings include
    b :: Proxy a -> Int
      (bound at Example.hs:10:1)

Есть библиотека для решения равенств ghc-typelits-natnormalise , но не неравенства.

1 Ответ

1 голос
/ 31 марта 2019

Несмотря на описание пакета, ghc-typelits-natnormalise также может решить неравенства.Следующие типы программ проверяются с помощью GHC 8.6.4 и ghc-typelits-natnormalise-0.6.2: 

{-# LANGUAGE KindSignatures, TypeOperators, ScopedTypeVariables,
             DataKinds, TypeFamilies #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise -Wall #-}

import GHC.TypeNats
import Data.Proxy

a :: forall (a :: Nat). 1 <= a => Proxy a -> Int
a = undefined

b :: forall (a :: Nat). 2 <= a => Proxy a -> Int
b = a
...