ฉันจะบอก GHC ให้เป็นไปตามข้อ จำกัด ระดับประเภท <= ได้อย่างไรถ้าฉันรู้ว่าเป็นจริงในรันไทม์

Aug 17 2020

ฉันมีประเภทพาราเมตไตรด้วยจำนวนธรรมชาติn:

data MyType (n :: Nat) = MyType

การดำเนินการในประเภทนี้จะสมเหตุสมผลก็ต่อเมื่อn > 0ดังนั้นฉันจึงระบุว่าเป็นข้อ จำกัด :

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

(หมายเหตุว่ารุ่นที่แท้จริงของฟังก์ชั่นเหล่านี้จะทำการใช้งานnโดยเปลี่ยนมันเป็นค่าที่มีnatVal.)

ฉันต้องการสร้างประเภทอัตถิภาวนิยม ( SomeMyType) ที่ให้เราเลือกnที่รันไทม์:

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

เพื่อสร้างค่าของSomeMyTypeฉันกำลังเขียนsomeMyTypeValฟังก์ชันที่ใช้งานได้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

สิ่งนี้จะทำงานได้ดีอย่างสมบูรณ์โดยไม่มี1 <= nข้อ จำกัด แต่ด้วยข้อ จำกัด ฉันได้รับข้อผิดพลาดประเภทต่อไปนี้:

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

ฉันจะหลีกเลี่ยงข้อ จำกัด นี้ได้อย่างไร ตั้งแต่ผมได้ตรวจสอบว่าn > 0ที่รันไทม์ฉันจะไม่คิดใช้การดำเนินการเช่นunsafeCoerceที่นี่เพื่อโน้มน้าว GHC ว่า1 <= nเป็นความจริง แต่ฉันไม่สามารถเพียงแค่ใช้เพราะที่จะสูญเสียค่าชนิดระดับunsafeCoercen

วิธีที่ดีที่สุดในการจัดการกับสิ่งนี้คืออะไร?

คำตอบ

6 TikhonJelvis Aug 17 2020 at 05:21

หลังจาก poking รอบมากขึ้นอีกนิดผมพบคำตอบที่จัสติน L's กับคำถามที่คล้ายกัน เขาห่อโซลูชันของเขาไว้ในtypelits-witnessesแพ็คเกจซึ่งฉันสามารถใช้เพื่อแก้ปัญหานี้ได้อย่างหมดจด:

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 %<=? bให้เราเปรียบเทียบจำนวนธรรมชาติสองระดับและให้คำพยานแก่เราว่าaน้อยกว่าb( LE) หรือไม่ ( NLE) สิ่งนี้ทำให้เรามีข้อ จำกัด พิเศษในLEกรณีที่จะส่งคืน a SomeMyTypeแต่การพยายามทำเช่นนั้นในNLEกรณีนี้จะทำให้เรามีข้อผิดพลาด "ไม่ตรงกัน" 1 <=? n 'กับ' 'จริง' '

สังเกตลายเซ็นประเภทที่ชัดเจนสำหรับcheck- หากไม่มีมันประเภทของcheckจะถูกอนุมานเป็นcheck :: SomeNat -> Maybe aและฉันจะได้รับข้อผิดพลาดประเภทต่อไปนี้:

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

ด้วยลายเซ็นประเภทที่ชัดเจนทุกอย่างใช้งานได้และรหัสยังอ่านได้ (สมเหตุสมผล)

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

เป็นคำตอบที่ตรงมากขึ้น, ข้อ จำกัดเป็นเพียงนามแฝงประเภทสำหรับ1 <= n 1 <=? n ~ 'Trueคุณสามารถสร้างข้อ จำกัด ด้านความเท่าเทียมกันได้อย่างไม่ปลอดภัยด้วย:

{-# LANGUAGE DataKinds, TypeOperators #-}

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

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

ซึ่งไม่มากก็น้อยสิ่งที่typelits-witnessesกำลังทำอยู่ภายใต้ประทุน

ด้วยคำจำกัดความดังกล่าวสิ่งต่อไปนี้ควรพิมพ์ - ตรวจสอบ:

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