Bagaimana saya bisa memberitahu GHC untuk memenuhi batasan tipe-level <= jika saya tahu itu benar saat runtime?

Aug 17 2020

Saya memiliki tipe parametrized dengan bilangan asli n:

data MyType (n :: Nat) = MyType

Operasi pada tipe ini hanya masuk akal jika n > 0, jadi saya menetapkannya sebagai batasan:

myFunction :: (KnownNat n, 1 <= n) => MyType n -> MyType n
myFunction = id

(Perhatikan bahwa versi sebenarnya dari fungsi ini memang digunakan ndengan mengubahnya menjadi nilai dengan natVal.)

Saya ingin membuat tipe eksistensial ( SomeMyType) yang memungkinkan kita memilih nsaat runtime:

data SomeMyType where
  SomeMyType :: forall n. (KnownNat n, 1 <= n) => MyType n -> SomeMyType

Untuk menghasilkan nilai SomeMyType, saya menulis someMyTypeValfungsi yang berfungsi seperti someNatVal:

someMyTypeVal :: Integer -> Maybe SomeMyType
someMyTypeVal n
  | n > 0 = case someNatVal n of
      Just (SomeNat (_ :: p n)) -> Just (SomeMyType (MyType @n))
      Nothing                   -> Nothing
  | otherwise = Nothing

Ini akan bekerja dengan baik tanpa 1 <= nkendala, tetapi dengan kendala saya mendapatkan jenis kesalahan berikut:

• Couldn't match type ‘1 <=? n’ with ‘'True’
    arising from a use of ‘SomeMyType’

Bagaimana cara mengatasi batasan ini? Karena saya telah memeriksanya n > 0pada waktu proses, saya tidak keberatan menggunakan operasi seperti di unsafeCoercesini untuk meyakinkan GHC bahwa 1 <= nitu benar — tetapi saya tidak bisa menggunakannya begitu sajaunsafeCoerce karena itu akan kehilangan nilai level-tipe n.

Apa cara terbaik untuk mengatasi ini?

Jawaban

6 TikhonJelvis Aug 17 2020 at 05:21

Setelah mencari-cari lebih banyak, saya menemukan jawaban Justin L. untuk pertanyaan serupa . Dia membungkus solusinya ke dalam typelits-witnessespaket yang dapat saya gunakan untuk menyelesaikan masalah ini dengan cukup bersih:

someMyTypeVal :: Integer -> Maybe SomeMyType
someMyTypeVal n = someNatVal n >>= check
  where check :: SomeNat -> Maybe SomeMyType
        check (SomeNat (_ :: p n)) = case (SNat @1) %<=? (SNat @n) of
          LE Refl -> Just (SomeMyType (MyType @n))
          NLE _ _ -> Nothing

a %<=? bmari kita bandingkan dua bilangan asli tingkat tipe dan memberi kita kesaksian apakah akurang dari b( LE) atau tidak ( NLE). Ini memberi kita batasan ekstra LEuntuk mengembalikan a SomeMyType, tetapi mencoba melakukan itu dalam NLEkasus masih akan memberi kita kesalahan "tidak bisa mencocokkan '1 <=? N' dengan '' Benar '".

Perhatikan tanda tangan tipe eksplisit untuk check—tanpa itu, tipe checkdisimpulkan sebagai check :: SomeNat -> Maybe adan saya akan mendapatkan kesalahan tipe berikut:

• Couldn't match type ‘a’ with ‘SomeMyType’
   ‘a’ is untouchable
     inside the constraints: 'True ~ (1 <=? n)

Dengan tanda tangan tipe eksplisit semuanya bekerja dan kodenya bahkan (cukup) dapat dibaca.

1 K.A.Buhr Aug 19 2020 at 05:24

Sebagai jawaban yang lebih langsung, batasan 1 <= nhanyalah alias tipe untuk 1 <=? n ~ 'True. Anda dapat membuat batasan kesetaraan jenis dengan tidak aman dengan:

{-# LANGUAGE DataKinds, TypeOperators #-}

import Data.Type.Equality
import GHC.TypeLits
import Unsafe.Coerce

unsafeDeclarePositive :: p n -> (1 <=? n) :~: 'True
unsafeDeclarePositive _ = unsafeCoerce Refl

yang kurang lebih apa typelits-witnessesyang dilakukan di bawah tenda.

Dengan definisi itu di tempat, yang berikut harus mengetik-periksa:

someMyTypeVal :: Integer -> Maybe SomeMyType
someMyTypeVal n
  | n > 0 = case someNatVal n of
      Just (SomeNat (pxy :: p n)) ->
        case unsafeDeclarePositive pxy of
          Refl -> Just (SomeMyType (MyType @n))
      Nothing -> Nothing
  | otherwise = Nothing