什么是辛德雷-米尔纳?

StackOverflow https://stackoverflow.com/questions/399312

题

我遇到这个术语 辛德雷-米尔纳, 我不确定如果把握这意味着什么。

我读以下员额：

但没有一个单一进入这个术语在维基百科通常提供给我一个简洁的解释。
注意到 -有人 现在已经加入

这是什么？
什么样的语言和工具落实或使用它？
请你提供一个简明的答案吗？

有帮助吗？

解决方案

辛德雷-米纳是一个 类型的系统 发现独立的罗杰*辛德雷(谁在看逻辑)，并后来通过罗宾*米尔纳(卫生组织正在编程语言)。优点辛德雷-米尔纳都是

  • 它支持 多形态 功能；例如，一个功能，可以给你的长度单独的类型要素，或者一个职能没有一个二元树查独立的类型的钥储存在树。

  • 有时候，一个函数或价值可以有 多种类型, 如在例的长度功能：它可以是"整数列表的整"、"列表的串整数"、"列表的对于整数"，等等。在这种情况下，一个信号优势的辛德雷-米尔纳的系统， 每个良好的类型期有一个唯一的"最好的"的类型, ，这就是所谓的 主要的类型.主要类型的清单长度的函数"任何 a, 、职能从清单 a 以整数".在这里， a 是一个所谓的"类型参数"，这是 明确氧微积分 但 隐含在最编程语言.使用的类型参数的解释了为什么辛德雷-米纳是一个系统，实现了 参数化 多态性.(如果你写一个定义的长度功能在毫升，你就可以看到类型参数，因此：

     fun 'a length []      = 0
   | 'a length (x::xs) = 1 + length xs

  • 如果 一术语具有一个辛德雷-米诺的类型，然后 主要的类型可以推断，而不需要任何类型的声明 或其他注释由程序员。(这是一个混合福，因为任何人都可以证明，曾经处理的一大块毫升的代码有没有注解。)

辛德雷-米诺是基础型的系统的几乎每一个静态地输入功能的语言。这样的语言，在共同使用包括

所有这些语言都有扩展的辛德雷-米诺;Haskell，清洁和客观的加枫这样做的雄心勃勃和不寻常的方式。(扩展是需要处理可变的变量，由于基本辛德雷-米尔纳可以颠复使用，例如，一个可变的小区保持一个值的列表未说明的类型。这些问题都涉及通过扩展叫 值的限制.)

许多其他小的语言和工具的基础上输入功能的语言的使用辛德雷-米尔纳。

辛德雷-米纳是一个限制 F系统, ，允许多种类型，但这 需要注释，由程序员.

其他提示

你可能能够找到原始文件使用Google学者或CiteSeer--或当地的大学图书馆。第一是够老了，你可能必须找到约束的副本杂志，我找不到它在线。链接，我找到另一个被打破的，但可能有其他人。你会肯定能够找到文件引用了这些。

辛德雷，罗杰J, 主要类型方案中的一个对象组合逻辑, 交易的美国数学学会，1969年。

米诺罗宾 一个理论上的类型多, 《计算机和系统科学学院，1978年。

简单的辛德雷-米尔纳类型的推断实施在C#:

辛德雷-米尔纳类型推理过(口齿不清上下)的S-表情，在下650线C#

注意到执行的范围内的只有270或所线C#(为算法W适当和少数几个数据结构，以支持它，无论如何)。

使用的摘录：

    // ...

    var syntax =
        new SExpressionSyntax().
        Include
        (
            // Not-quite-Lisp-indeed; just tolen from our host, C#, as-is
            SExpressionSyntax.Token("\\/\\/.*", SExpressionSyntax.Commenting),
            SExpressionSyntax.Token("false", (token, match) => false),
            SExpressionSyntax.Token("true", (token, match) => true),
            SExpressionSyntax.Token("null", (token, match) => null),

            // Integers (unsigned)
            SExpressionSyntax.Token("[0-9]+", (token, match) => int.Parse(match)),

            // String literals
            SExpressionSyntax.Token("\\\"(\\\\\\n|\\\\t|\\\\n|\\\\r|\\\\\\\"|[^\\\"])*\\\"", (token, match) => match.Substring(1, match.Length - 2)),

            // For identifiers...
            SExpressionSyntax.Token("[\\$_A-Za-z][\\$_0-9A-Za-z\\-]*", SExpressionSyntax.NewSymbol),

            // ... and such
            SExpressionSyntax.Token("[\\!\\&\\|\\<\\=\\>\\+\\-\\*\\/\\%\\:]+", SExpressionSyntax.NewSymbol)
        );

    var system = TypeSystem.Default;
    var env = new Dictionary<string, IType>();

    // Classic
    var @bool = system.NewType(typeof(bool).Name);
    var @int = system.NewType(typeof(int).Name);
    var @string = system.NewType(typeof(string).Name);

    // Generic list of some `item' type : List<item>
    var ItemType = system.NewGeneric();
    var ListType = system.NewType("List", new[] { ItemType });

    // Populate the top level typing environment (aka, the language's "builtins")
    env[@bool.Id] = @bool;
    env[@int.Id] = @int;
    env[@string.Id] = @string;
    env[ListType.Id] = env["nil"] = ListType;

    //...

    Action<object> analyze =
        (ast) =>
        {
            var nodes = (Node[])visitSExpr(ast);
            foreach (var node in nodes)
            {
                try
                {
                    Console.WriteLine();
                    Console.WriteLine("{0} : {1}", node.Id, system.Infer(env, node));
                }
                catch (Exception ex)
                {
                    Console.WriteLine(ex.Message);
                }
            }
            Console.WriteLine();
            Console.WriteLine("... Done.");
        };

    // Parse some S-expr (in string representation)
    var source =
        syntax.
        Parse
        (@"
            (
                let
                (
                    // Type inference ""playground""

                    // Classic..                        
                    ( id ( ( x ) => x ) ) // identity

                    ( o ( ( f g ) => ( ( x ) => ( f ( g x ) ) ) ) ) // composition

                    ( factorial ( ( n ) => ( if ( > n 0 ) ( * n ( factorial ( - n 1 ) ) ) 1 ) ) )

                    // More interesting..
                    ( fmap (
                        ( f l ) =>
                        ( if ( empty l )
                            ( : ( f ( head l ) ) ( fmap f ( tail l ) ) )
                            nil
                        )
                    ) )

                    // your own...
                )
                ( )
            )
        ");

    // Visit the parsed S-expr, turn it into a more friendly AST for H-M
    // (see Node, et al, above) and infer some types from the latter
    analyze(source);

    // ...

...这将产生:

id : Function<`u, `u>

o : Function<Function<`z, `aa>, Function<`y, `z>, Function<`y, `aa>>

factorial : Function<Int32, Int32>

fmap : Function<Function<`au, `ax>, List<`au>, List<`ax>>

... Done.

也参看 布莱恩*麦凯的JavaScript执行情况 关于健康，这也有助于开始(工作对我来说).

'禾田,

许可以下： CC-BY-SA 和 归因
不隶属于 StackOverflow
scroll top