ฉันจะบอก GHC ให้เป็นไปตามข้อ จำกัด ระดับประเภท <= ได้อย่างไรถ้าฉันรู้ว่าเป็นจริงในรันไทม์
ฉันมีประเภทพาราเมตไตรด้วยจำนวนธรรมชาติ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
เป็นความจริง แต่ฉันไม่สามารถเพียงแค่ใช้เพราะที่จะสูญเสียค่าชนิดระดับunsafeCoerce
n
วิธีที่ดีที่สุดในการจัดการกับสิ่งนี้คืออะไร?
คำตอบ
หลังจาก 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 <= 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