كيف يمكنني تبسيط هذا النوع?

Question

liftM2 {A B R : Set} {m} {x : Monad m} (f : A -> B -> R) (ma : m A) (mb : m B) : (m R)

هل هناك أي حيل للحد من هذا النوع?لدي زائدة عن الحاجة x هناك.

موناد هو نوع الفئة: (Set -> Set) -> Type

Answer 1

هذا أقصر ولكن ليس أكثر فائدة...

liftM2 {A B R} {m} : Monad m -> (A -> B -> R) -> m A -> m B -> m R.

أنا لا أفهم لماذا تريد أو تحتاج هذا أقصر مما هو عليه على الرغم من.كل شيء له أهميته ، والأسماء القليلة التي يتم الإدلاء بها تساعد في قراءتها أيضا.

هذا ليفتم 2 يبدو خفيفا كما يمكن أن يكون.

ومع ذلك ، إذا كنت تحدد الكثير من الوظائف التي تشترك جميعها في بعض المعلمات ، فيمكنك تحديدها داخل قسم ، يمكنك من خلاله الحصول على معلمات.على سبيل المثال ، انظر كيف يتم تعريف ليفتم 2 هنا:

http://mattam.org/repos/coq/oldprelude/Monad.v

ال mon : Monad m يتم تعريفه داخل القسم ، وسيتم تمريره إلى جميع الوظائف التي تستخدمه بالفعل.بمجرد إغلاق القسم ، يمكنك التحقق من التوقيع لمعرفة أنه تم تمريره بالفعل.

Answer 2

liftM2 {A B R : Set} `{Monad m} (f : A -> B -> R) (ma : m A) (mb : m B) : (m R)

أو

liftM2 `{Monad m} `(f : A -> B -> R) (ma : m A) (mb : m B) : (m R)

والثاني يغير ترتيب الحجج الضمنية ، لكنني أعتقد أنه معقول.

للحصول على شرح ل ' {} بناء الجملة ، انظر هنا.والفرق الرئيسي هو أن الاسم ، بدلا من نوع اختياري.بالإضافة إلى ذلك ، فإن السلوك الضمني للحجج غريب في الداخل ' {} ما لم تبدأ النوع مع !.