Mở đầu ML đƣợc tạo ra giữa những năm 1970 nhƣ một ngôn ngữ để xây dựng các bằng chứng trong Robin Milnerr‟s LCF (Lô-gic cho chức năng tính toán) máy tính hỗ trợ hệ thống hình thức lập luận. SML (ML tiêu chuẩn) đƣợc phát triển trong những năm đầu của những năm 1980 từ ML với phần mở rộng từ ngôn ngữ chức năng Hope định rõ. Giải thích SML bằng những ví dụ. Vì kí hiệu ˗ diện cho các kiểu hàm số, hệ thống ứng dụng SML và chỉ ra kết quả của việc tính một biểu thức nhƣ: - đổi từ một chƣơng trình SML cung cấp vài kiểu chuẩn các cơ chế để xác định các kiểu mới nhƣng chúng tôi sẽ không xem xét các kiểu đó ở đây.
Khi trình bày các đối tƣợng, SML luôn hiển thị các kiểu đi cùng các giá trị: <giá trị>: <kiểu> 4 fn: <kiểu> xây dựng nhƣ ta đã thảo luận về các kiểu cụ thể [1]. Kiểu Unit: Kiểu biểu thức với một kiểu cơ bản là định danh của kiểu Đơn vị kiểu chỉ có một phần tử, đƣợc viết nhƣ ngoặc rỗng: ():unit Giống void trong C, unit đƣợc sử dụng nhƣ kiểu kết quả cho hàm mà đƣợc thực hiện chỉ vì các tác động phụ. Kiểu unit cũng đƣợc sử dụng nhƣ kiểu của đối số cho hàm số mà không có đối số. Những lập trình viên C có thể sẽ bị lẫn bởi sự việc unit cho là có một phần tử, trong khi đó void có vẻ nhƣ không có phần tử nào.
Từ góc độ toán học, „một phần tử‟ là đúng đắn. Cụ thể, nếu hàm đƣợc giả thiết trả về. Tuy nhiên chúng ta không cần theo dõi hàm nhƣ vậy trả về giá trị nào, vì chỉ có một thứ mà nó có thể trả về. Hệ thống kiểu ML dựa trên nhiều năm nghiên cứu kiểu; hầu hết các khái niệm kiểu trong ML đã đƣợc xem xét rất cẩn thận [1, tr.
Kiểu Bool: Kiểu phép toán luận có định danh: bool và các 2 giá trị: true false (đúng sai) Ví dụ 1.1: > true:bool Biểu thức chung nhất liên kết với kiểu bool là biểu thức có điều kiện, với if e1 then e2 else e3 Có cùng kiểu với e2 và e3, nếu chúng có cùng kiểu và e1 có kiểu bool. Ở đây không có if-then mà không có else, cũng nhƣ biểu thức điều kiện cần phải có giá trị nếu phép kiểm tra điều kiện là đúng hoặc sai [1, tr. Kiểu Integer: Kiểu số nguyên có định danh: int với các giá trị nguyên dƣơng và nguyên âm Ví dụ 1.2: >42:int 5 ˗ ˜84 >84: int Chú ý việc sử dụng ˜ là dấu âm. Nhiều biểu thức nguyên đƣợc theo cách thông thƣờng, với hằng số và các phép toán số học chuẩn: 0, 1, 2,….-1, -2,…int +, -, *, div: int*int → int Phép toán div là phép toán nhị phân trung tố, đƣợc sử dụng nhƣ sau: fun quotien(x, y) = x div y; val quotien = fn: int*int → int Bản thân định danh div không phải là biểu thức.
Tƣơng tự, +, -, * cũng là các phép toán nhị phân trung tố [1, tr. Kiểu Real: Kiểu của ML cho số dấu phảy động là số thực. Để dễ dàng hiểu khi chúng ta suy luận kiểu, ML đòi hỏi phải có dấu chấm thập phân trong các hằng số thực: 1.44444,…real Các phép toán số học +, - và * có thể áp dụng cho số nguyên hoặc số thực. Ở đây chúng ta có một vài biểu thức ví dụ và đầu ra kết quả của chƣơng trình dịch [1, tr.
3 + 4; Val it = 7: int 4. Kiểu Bản ghi: Giống nhƣ bản ghi Pascal và cấu trúc C, bản ghi ML tƣơng tự nhƣ bộ, nhƣng với các thành phần có tên. Các giá trị và các kiểu của bản ghi đƣợc viết dạng ngoặc móc nhƣ sau: {First_name = "Donald", Last_name = "Knuth"}; val it = First_name = "Donald", Last_name = "Knuth"} :{ First_name: string, Last_name: string} Biểu thức ở đây có hai thành phần, một đƣợc gọi là First_name và thành phần thứ hai đƣợc gọi là Last_name. Kiểu của bản ghi cho ta biết kiểu của từng thành phần.
6 Các thành phần của bản ghi đƣợc truy cập bởi hàm # giống nhƣ bộ, nhƣng đƣợc gọi tên dựa theo tên của thành phần thay vì vị trí. Sau đây là ví dụ: #First_name ({First_name = "Donald", Last_name = "Knuth"}; Cách khác chọn các thành phần của bộ và bản ghi là sánh mẫu mà đƣợc mô tả trong mục sau. Danh sách (List) Danh sách của ML có độ dài tùy ý, nhƣng mọi phần tử của danh sách phải có cùng kiểu. Chúng ta có thể viết danh sách bằng cách liệt kê các phần tử của nó, tách nhau bởi dấu phẩy, bên trong ngoặc vuông.
Trong SML, không giống λ, một danh sách phải bao gồm các phần tử cùng loại và kết thúc với danh sách trống Danh sách đƣợc viết là chuỗi các phần tử riêng biệt bên trong [ và ].3: [1, 4, 9, 16, 25] [“ant”, “beetle”, “caterpillar”, “dragonfly”, “earwig”] Có một danh sách rỗng ngụ ý ở cuối danh sách: [ ] là danh sách rỗng. Danh sách rỗng đƣợc viết là nil trong ML. Kiểu biểu thức cho một danh sách phụ thuộc vào các loại phần tử Ví dụ đầu tiên ở trên: [1, 4, 9, 16, 25]; > Ví dụ thứ 2 ở trên: [ “ant”, “beetle”, “caterpillar”, “dragonfly”, “earwig”]; >[ “ant”, “beetle”, “caterpillar”, “dragonfly”, “earwig”]: sách các xâu. [[1, 1], [2, 8], [3, 27], [4, 64], [5, 125]]; >[[1, 1], [2, 8], [3, 27], [4, 64], [5, 125]]: danh s danh sách của danh sách số nguyên.
Sau đây là một số ví dụ danh sách các kiểu khác nhau: 7 Ví dụ 1.4: ["red","yellow","blue"]; val it = [“red","yellow","blue"]: string list [1, 2, 3, 4]; val it = [1, 2, 3, 4]: int list [true, false]; val it = [ true, false]: bool list [ fn x=> x+1, fn x=>x+2]; val it=[fn, fn]: (int->int) list Đối với danh sách ngắn, chƣơng trình dịch in ra các phần tử của danh sách khi chỉ ra rằng biểu thức danh sách đã đƣợc tính toán. Đối với danh sách dài, các phần tử cuối đƣợc thay thế bởi ba dấu chấm. Nhƣ ví dụ danh sách cuối ở trên chỉ ra có thể viết danh sách các hàm. Nói chung, t list là kiểu của danh sách, nếu mọi phần tử của nó có kiểu t [1, tr.
Các kiểu hàm số và biểu thức Một hàm số sử miền và vùng của nó: -> Chú ý việc sử dụng -> để chỉ tên ánh xạ của một hàm số. Trong SML, nhƣ trong phép toán λ và Lisp, các biểu thức thƣờng dựa trên ứng dụng các kí hiệu tiền tố hàm số với các hàm số có trƣớc các đố Các ứng dụng hàm số đƣ g [1, tr. Các hàm phủ định phép toán luận: not trả về dạng phủ định của phép toán luận đối số của nó, ví dụ: 8 not true; >false: bool Vì vậy, kiểu của not là: not; > fn: bool ->bool Phủ định đƣợc viết là not, hội là andalso và tuyển là orelse. Chẳng hạn, sau đây là hàm mà xác định xem hai biến bool của nó có cùng giá trị bool không, tiếp theo là biểu thức mà gọi hàm đó Ví dụ 1.5: fun equiv(x, y)= (x andalso y) orelse ((not x) andalso(not y)); val equiv = fn: bool * bool->bool equiv(true, false); val it = false: bool 1.
Hàm số chuẩn và operator overloading Ta nói các biến bool x và y có cùng giá trị bool, tức là chúng cùng true hoặc cùng false. Biểu thức con thứ nhất (x andalso y) là true nếu cả hai x và y cùng true và biểu thức con thứ hai ((not x) andalso (not y)) là true nếu cả hai cùng false. Nguyên nhân tên dài andalso và orelse là để nhấn mạnh thứ tự tính toán. Trong biểu thức (a andalso b) trong đó a và b là hai biểu thức; a đƣợc tính trƣớc, nếu a là true, thì b đƣợc tính tiếp.
Ngƣợc lại giá của biểu thức (a andalso b) là false mà không cần tính b. Tƣơng tự, b trong (a orelse b) chỉ đƣợc tính chỉ trong trƣờng hợp a là false.6: true orelse false; val it = true: bool true andalso false; val it = false: bool Hệ thống SML có thể không thể biểu diễn các loại của các toán tử này nhƣng chúng tỏ ra hiệu quả: fn: (bool* bool) -> bool vì vậy chúng đều có 2 đối số boolean, đƣợc xử lí nhƣ một: bool * bool tuple cho cú pháp trung tố, và trả về một kết quả Boolean. Chuỗi hàm chuẩn (String) Các xâu đƣợc viết nhƣ dãy các ký hiệu đƣợc bao quanh dấu ngoặc kép: "William Jefferson Clinton": string "Boris Yeltsin": string Nối xâu được viết dạng ^, như vậy ta có: "Chelsea"^""^"Clinton"; Val it=" Chelsea Clinton": string Nối 2 chuỗi lại với nhau: -op ^ ; >fn: (string * string) - > string Ví dụ 1.7: "happy" ^ "brithday!"; val it = "happy brithday!": string Toán tử: size trả về kích cỡ của 1 chuỗi size; >fn: string -> int Ví dụ: size "hello"; > 5: int Hàm chuẩn để chuyển chuỗi vào danh sách chuỗi đƣợc bàn luận dƣới đây. Các hàm chuẩn trên danh sách loại nào.
Trong SML, 1 loại không đƣợc ký hiệu bằng tên 1 chữ cái đứng trƣớc là dấu phẩy ´, ví dụ: ´a, ´b, ´c Vì vậy, ta có thể tham khảo danh sách các đối tƣợng gõ tùy ý nhƣ là loại đã có: ´a list Trong SML, danh sách đƣợc truy cập bởi các toán tử lấy đầu và lấy đuôi: hd, tl Toán tử đầu trả về đối tƣợng đứng đầu với kiểu: ´a từ 1 danh sách đƣợc gõ tùy ý. Vì vậy, hd sẽ là kiểu: hd; > fn: (´a list) - >´a Ví dụ: hd [1,2,3,4,5]; > 1: int; 10 Tƣơng tự, toán tử đuôi trả về đuôi với kiểu: ´a list từ 1 danh sách gõ tùy ý. Vì vậy, tl sẽ là kiểu: tl; > fn: (´a list) -> (´a list) Ví dụ 1.8: tl [“alpha”, “beta”, “gamma”, “delta”, “epsilon”]; > [“alpha”, “beta”, “gamma”, “delta”, “epsilon”]: string list Các toán tử xâu chuỗi các danh sách trung tố là: :: Cho một đối tƣợng và một danh sách các đối tƣợng cùng loại, :: trả về một danh sách mới với đối tƣợng ở đầu và danh sách đối tƣợng ở đuôi. Vì vậy, :: có kiểu: op::; >(´ a*(´a list)) - > (´ a list) Ví dụ 1.9: 0::[1, 2, 3, 4, 5]; > [0, 1, 2, 3, 4, 5]: int list Các toán tử hd và tl đƣợc gọi là đa hình (polymorphic) vì chúng ứng dụng cho một danh sách của bất kì kiểu nào của đối tƣợng.
Suy luận kiểu Suy luận kiểu là quá trình xác định kiểu của biểu thức dựa trên các kiểu đã biết của các ký hiệu xuất hiện trong các biểu thức đó. Sự khác nhau giữa suy luận kiểu và kiểm tra kiểu thời gian dịch là ở mức độ. Thuật toán kiểm tra kiểu duyệt qua chƣơng trình kiểm tra các kiểu khai báo bởi lập trình viên.