تستنتج خوارزمية التوحيد أنواعًا محددة جدًا
-
22-12-2019 - |
سؤال
كنت أحاول إنشاء مجموعات من الحجم n في إدريس:
module NTuple
data Tuple : Vect n Type -> Type where
EmptyTuple : Tuple Nil
TupleItem : a -> Tuple types -> Tuple (a :: types)
mapN : {types : Vect n Type} -> (i : Fin (S n)) -> (a -> b) -> Tuple (insertAt i a types) -> Tuple (insertAt i b types)
mapN fZ f (TupleItem x xs) = TupleItem (f x) xs
mapN (fS i) f (TupleItem x xs) = TupleItem x (mapN i f xs)
لكني أتلقى هذا الخطأ في السطر الأخير:
When elaborating left hand side of mapN: When elaborating an application of NTuple.mapN: Can't unify Tuple (a :: types) with Tuple (insertAt (fS i) a types) Specifically: Can't unify a :: types with insertAt (fS i) a types
هل هناك طريقة لجعل هذه الوظيفة تعمل؟
المحلول
المشكلة هي insertAt (FS i) a types
لا يمكن تخفيضها دون معرفة أي شيء عنها types
.لو علمنا types = t :: ts
ثم يمكن تخفيضه إلى t :: insertAt i ts
.
لكن في الحالة الثانية mapN
, ، نحن يفعل إعلم أن types
هو بالضبط من هذا الشكل:
- حجتنا الأولى هي
FS i
- ضمنا
n = S m
بالنسبة للبعضm
... - يعني ضمنا لدينا
types
الوسيطة لها نوعVect (S m) Type
- مما يعني أنه من الشكل
t :: ts
!
وبمجرد أن نشير إلى ذلك لإدريس، فإنه يسعد بالتخفيض insertAt (FS i) a types
وبالتالي، يتم التحقق من نوع التعليمات البرمجية الخاصة بك:
mapN : {types : Vect n Type} -> (i : Fin (S n)) -> (a -> b) -> Tuple (insertAt i a types) -> Tuple (insertAt i b types)
mapN FZ f (TupleItem x xs) = TupleItem (f x) xs
mapN {types = _ :: _} (FS i) f (TupleItem x xs) = TupleItem x (mapN i f xs)
mapN {types = []} (FS i) _ _ = absurd i
لا تنتمي إلى StackOverflow