ما الذي يسبب هذا الخطأ نوع المعيار ML؟

Question

كنت أحاول جعل إصدار ذيل عريض من هذه وظيفة SML بسيطة للغاية:

fun suffixes [] = [[]]
  | suffixes (x::xs) = (x::xs) :: suffixes xs;

أثناء هذا، كنت أستخدم التعليقات التوضيحية النوعية على المعلمات. يظهر الكود التالي هذا، ويسبب خطأ في الكتابة (الواردة أدناه)، في حين إذا قمت ببساطة بإزالة التعليقات التوضيحية النوعية، فإن SML تقبلها دون أي مشكلة، وإعطاء الوظيفة كلها نفس التوقيع مثل الوظيفة الأكثر بساطة أعلاه.

fun suffixes_tail xs =
    let
        fun suffixes_helper [] acc = []::acc
          | suffixes_helper (x::xs:'a list) (acc:'b list) =
                suffixes_helper xs ((x::xs)::acc)
    in
        suffixes_helper xs []
    end;

خطأ:

$ sml typeerror.sml 
Standard ML of New Jersey v110.71 [built: Thu Sep 17 16:48:42 2009]
[opening typeerror.sml]
val suffixes = fn : 'a list -> 'a list list
typeerror.sml:17.81-17.93 Error: operator and operand don't agree [UBOUND match]
  operator domain: 'a list * 'a list list
  operand:         'a list * 'b list
  in expression:
    (x :: xs) :: acc
typeerror.sml:16.13-17.94 Error: types of rules don't agree [UBOUND match]
  earlier rule(s): 'a list * 'Z list list -> 'Z list list
  this rule: 'a list * 'b list -> 'Y
  in rule:
    (x :: xs : 'a list,acc : 'b list) =>
      (suffixes_helper xs) ((x :: xs) :: acc)
/usr/local/smlnj-110.71/bin/sml: Fatal error -- Uncaught exception Error with 0
 raised at ../compiler/TopLevel/interact/evalloop.sml:66.19-66.27

هناك خطيان معينان. يبدو أن هذا الأخير أقل أهمية هنا، وهو عدم تطابق بين بنودين اللاحقين. الأول هو الشخص الذي لا أفهمه. أنا أعلم أن أذكر أن المعلمة الأولى هي من النوع 'a:list وأن المعلمة الثانية من النوع 'b:list. وبعد لا ينبغي أن تكون خوارزمية الاستدلال من نوع Hindleyner، والتي بنيت من أعلى التوحيد العام كما أفهمها، تكون قادرة على توحيد 'b:list مع 'a:list list, باستخدام استبدال 'b ---> 'a list?

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

fun suffixes_helper [] acc = []::acc
    | suffixes_helper (x::xs) acc =
          suffixes_helper (xs:'a list) (((x::xs)::acc):'b list);

الخطأ هو الآن:

typeerror.sml:5.67-5.89 Error: expression doesn't match constraint [UBOUND match]
  expression: 'a list list
  constraint: 'b list
  in expression:
    (x :: xs) :: acc: 'b list

Answer 1

لست متأكدا من SML، ولكن F #، لغة وظيفية أخرى، تعطي تحذيرا في هذا النوع من الموقف. قد يكون إعطاء خطأ قاسيا قليلا، لكنه منطقي: إذا قدم المبرمون متغيرا إضافيا نوعا إضافيا "B، وإذا كان" B من النوع "، قد لا تكون الوظيفة عامة مثل المبرمج المقصود يستحق التقارير.

Answer 2

هذا يعمل:

fun suffixes_tail xs =
    let
        fun suffixes_helper [] acc = []::acc
          | suffixes_helper (x::xs:'a list) (acc:'a list list) =
                suffixes_helper xs ((x::xs)::acc)
    in
        suffixes_helper xs []
    end

كما يقول Joh و Newacct، 'b list فضفاضة جدا. عندما تعطي الشرح النوع التوضيحي

fun suffixes_helper (_ : 'a list) (_ : 'b list) = ...

كمي ضمنيا كما

fun suffixes_helper (_ : (All 'a).'a list) (_ : (All 'b).'b list) = ...

ومن الواضح 'b = 'a list لا يمكن أن يكون صحيحا (All a') و (All b') الوقت ذاته.

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

Answer 3

عند استخدام متغيرات النوع مثل 'a و 'b, ، هذا يعني أن 'a و 'b يمكن ضبطها على اى شى, بشكل مستقل. وبعد لذلك على سبيل المثال، يجب أن تعمل إذا قررت ذلك 'b كان int و 'a كان float; ؛ ولكن من الواضح أن هذا غير صالح في هذه الحالة لأنه اتضح ذلك 'b يجب أن يكون 'a list.