Dependent ML

Dependent ML (DML) is an experimental, multi-paradigm, general-purpose, high-level, functional programming language proposed by Hongwei Xi (Xi 2007) and Frank Pfenning. It is a dialect of the programming language ML. Dependent ML extends ML by a restricted notion of dependent types: types may be dependent on static indices of type Nat (natural numbers). Dependent ML employs a constraint theorem prover to decide a strong equational theory over the index expressions.

DML's types are not dependent on runtime values - there is still a phase distinction between compilation and execution of the program.[1] By restricting the generality of full dependent types type checking remains decidable, but type inference becomes undecidable.

Dependent ML has been superseded by ATS and is no longer under active development.

References

  1. ^ Aspinall & Hofmann 2005. p. 75.

Further reading

  • Xi, Hongwei (March 2007). "Dependent ML: An Approach to Practical Programming with Dependent Types". Journal of Functional Programming. 17 (2): 215–286. doi:10.1017/S0956796806006216. S2CID 45996427.
  • David Aspinall and Martin Hofmann [de] (2005). "Dependent Types". In Pierce, Benjamin C. (ed.) Advanced Topics in Types and Programming Languages. MIT Press.


Stub icon

This programming-language-related article is a stub. You can help Wikipedia by expanding it.

Read other articles:

有楽町スバル座

有楽町スバル座Yurakucho Subaru-za 有楽町スバル座が入居する有楽町ビルヂング情報正式名称 有楽町スバル座完成 1966年開館 1966年4月27日開館公演 青春のお通り 愛して泣いて突っ走れ![1]閉館 2019年10月20日最終公演 花筐/HANAGATAMI収容人員 272人設備 ドルビーデジタル5.1ch、DLP用途 映画上映運営 スバル興業株式会社所在地 〒100-0006東京都千代田区有楽町1-10-1有楽町ビルヂン

 

Аніта Лонсбро

Аніта ЛонсброAnita LonsbroughЗагальна інформаціяГромадянство  Велика БританіяНародження 10 серпня 1941(1941-08-10) (82 роки)Гаддерсфілд, Велика БританіяЗріст 178 смAlma mater St. Joseph's Catholic College, BradforddСпортВид спорту спортивне плавання Участь і здобутки Нагороди Міжнародний зал слави пл

 

Shire of Toodyay

Shire of Toodyay Local Government Area van Australië Locatie van Shire of Toodyay in West-Australië Situering Staat West-Australië Hoofdplaats Toodyay Coördinaten 31°33'4ZB, 116°27'50OL Algemene informatie Oppervlakte 1693,8 km² Inwoners 4.601 (2021)[1] Overig Wards 4 Website (en) Shire of Toodyay Portaal    Australië Shire of Toodyay is een lokaal bestuursgebied (LGA) in de regio Wheatbelt in West-Australië. De hoofdplaats is Toodyay. Districtsgebouw (2014) Geschie...

2022年紐約線上影評人協會獎

第23屆紐約在線影評人協會獎日期2021年12月11日 (2021-12-11)地点美國紐約州紐約摘要最佳電影《伊尼舍林的女妖》获獎最多《伊尼舍林的女妖》（6項） ← 22屆 紐約在線影評人協會獎 24屆 → 第23屆紐約在線影評人協會獎（英語：The 23rd New York Film Critics Online Awards）旨在表揚2022年優秀的電影作品，於2022年12月11日宣布得獎名單[1][2]。 得獎名單 最佳導演

 

Our Lady of Aberdeen

Our Lady of Aberdeen St Mary's Cathedral Huntly Street Aberdeen Our Lady of Aberdeen is a type of Madonna and Child statuettes copied from the Notre Dame du Bon Succès statuette located in Brussels. Such replicas are to be found across the North East of Scotland. History It is believed that the statue in Brussels may have been in Old Aberdeen as early as 1450. References to a statue in a Chapel at the Bridge of Dee in Aberdeen suggest that it may have been placed there by Bishop Gavin Dunbar...

 

List of lowest-income places in the United States

This article's factual accuracy is disputed. Relevant discussion may be found on the talk page. Please help to ensure that disputed statements are reliably sourced. (April 2023) (Learn how and when to remove this template message) In 2017, Comerío Zona Urbana in Comerío, Puerto Rico had the lowest median household income of any place with more than 1,000 people in the United States[contradictory][note 1] This article is part of a series onIncome in theUnited States of Americ...

جامع الإمام موسى الكاظم

هذه المقالة يتيمة إذ تصل إليها مقالات أخرى قليلة جدًا. فضلًا، ساعد بإضافة وصلة إليها في مقالات متعلقة بها. (سبتمبر 2017) جامع الإمام موسى الكاظم إحداثيات 30°30′04″N 47°46′56″E / 30.5011°N 47.7821°E / 30.5011; 47.7821  معلومات عامة القرية أو المدينة البصرة/ الحيانية الدولة العراق الم

 

Kedutaan Besar Republik Indonesia di London

Kedutaan Besar Republik Indonesia di LondonEmbassy of the Republic of Indonesia in LondonKoordinat51°30′38″N 0°09′06″W / 51.5106°N 0.1517°W / 51.5106; -0.1517Lokasi Westminster, London, UKAlamatTrevelyan House30 Great Peter StreetLondon SW1P 2BUUnited KingdomDuta BesarDesra PercayaYurisdiksi Inggris Irlandia Irlandia Utara Skotlandia WalesSitus webkemlu.go.id/london/id Kedutaan Besar Republik Indonesia di London (KBRI London) (bahas...

 

Martino's Summer

FilmMartino’s SummerDirected byMassimo NataleCinematographyVladan RadovicRunning time90 minutes Martino's Summer (Italian: L’estate di Martino) is a 2010 Italian drama film directed by Massimo Natale.[1][2] It won the Audience Award at the 2011 Flaiano Prizes.[3] It tells the story of a young man in southern Italy who has a romance with a vacationer from the north and learns to surf from an officer on a U.S. military base. Cast Treat Williams: Captain Jeff Clark Lu...

Pertempuran Leipzig

Pertempuran LeipzigBagian dari Perang Koalisi Keenam, 1812-1814Peta Pertempuran tanggal 18 Oktober 1813, dari Ensiklopedia MeyersTanggal16 Oktober–19 Oktober 1813LokasiLeipzig, SachsenHasil Kemenangan pihak koalisiPihak terlibat  Prancis Kadipaten Warsawa Konfederasi Rhine : Kerajaan Saxon  Rusia  Austria Prusia SwediaTokoh dan pemimpin  Prancis : Napoleon Bonaparte Polandia : Jozef Antoni Poniatowski Saxon : Frederick Augustus I  Austr...

 

Seiko

Japanese manufacturing company This article is about the Japanese company. For other uses, see Seiko (disambiguation). Seiko Group CorporationSeiko's Wako store in Ginza serves as the company's registered office.Native nameセイコーグループ株式会社Romanized nameSeikō Gurūpu kabushiki gaishaFormerlyK. Hattori & Co. (1881-1917)K. Hattori & Co., Ltd. (1917-1983)Hattori Seiko Co., Ltd. (1983-1990)Seiko Corporation (1990-2007)Seiko Holdings Corporation (2007-2022)TypePublic (K...

 

No. 315 Polish Fighter Squadron

315 Squadron redirects here. For the Indian Naval Air Arm squadron, see INAS 315. No. 315 (City of Dęblin) Polish Fighter Squadron315 Squadron LogoActive21 January 1941 – 14 January 1947Country United KingdomAllegiance Polish government in exileBranch Royal Air ForceRoleFighter SquadronPart ofRAF Fighter CommandNickname(s)DeblinDywizjon Myśliwski DęblińskiCommandersNotablecommandersEugeniusz HorbaczewskiInsigniaSquadron CodesPK (Jan 1941 – Jan 1946)Military unit No. 315 (City of ...

العلاقات العراقية الناوروية

العلاقات العراقية الناوروية العراق ناورو   العراق   ناورو تعديل مصدري - تعديل   العلاقات العراقية الناوروية هي العلاقات الثنائية التي تجمع بين العراق وناورو.[1][2][3][4][5] مقارنة بين البلدين هذه مقارنة عامة ومرجعية للدولتين: وجه المقارنة العرا...

 

Hailuogou

Glacier in China HailuogouA panorama of the HailuogouHailuogouTypeMountain glacierLocationDaxue Mountains, Sichuan, ChinaCoordinates29°34′01″N 101°57′00″E / 29.567°N 101.950°E / 29.567; 101.950 Hailuogou (Chinese: 海螺沟; pinyin: Hǎiluógōu; lit. 'Sea conch ravine'; Tibetan: དུང་དཀར་ལུང་པ, Wylie: dung dkar lung pa, THL: Dungkar Lungpa) is a glacier located in Luding County, Garzê Tibetan Autonomous Prefecture,...

 

MPG Media

PT Tiga Visi UtamaNama dagangMPG MediaJenisPublikIndustriMediaPendahuluMilestone Pacific GroupDidirikan2001; 21 tahun lalu (2001)PendiriJulius RuslanKantorpusatJakarta, IndonesiaTokohkunciDenise TjokrosaputroSistha Alicia TjokrosaputroProdukRadioSitus onlinePenerbitanPeriklananManajemen artisPemilikParamount EnterpriseSitus webwww.mpgmedia.co.id MPG Media merupakan salah satu perusahaan penerbitan dengan pertumbuhan tercepat di kawasan ini, MPG Media Publishing menciptakan konten untuk b...

A Piece of Your Mind

A Piece of Your MindPoster promosiHangul반의 반 GenreMelodramaDitulis olehLee Sook-yeonSutradaraLee Sang-yeobPemeranJung Hae-inChae Soo-binLee Ha-naKim Sung-kyuNegara asalKorea SelatanBahasa asliKoreaJmlh. episode12[a]ProduksiRumah produksiThe UnicornMovie RockDistributortvNRilis asliJaringantvNFormat gambar1080i (HDTV)Format audioDolby DigitalRilis23 Maret (2020-03-23) –28 April 2020 (2020-4-28) A Piece of Your Mind (Hangul: 반의 반; RR: B...

 

Juste Brouzes

French footballer Juste Brouzes Juste Brouzes (striped jersey)Personal informationDate of birth (1894-01-20)20 January 1894[1]Place of birth Paris, FranceDate of death 28 February 1973(1973-02-28) (aged 79)International careerYears Team Apps (Gls) France Juste Brouzes (20 January 1894 – 28 February 1973) was a French footballer. He competed in the men's tournament at the 1928 Summer Olympics.[2] References ^ Juste Brouzes at Olympedia ^ Evans, Hilary; Gjerde, Arild;...

 

Kidō Senshi Gundam: Senshitachi no Kiseki

Cet article est une ébauche concernant le jeu vidéo. Vous pouvez partager vos connaissances en l’améliorant (comment ?) (voir l’aide à la rédaction). Kidō Senshi GundamSenshitachi no KisekiDéveloppeur CapcomÉditeur BandaiDate de sortie JAP : 18 mars 2004 Franchise Mobile Suit GundamGenre Tir à la première personneMode de jeu Un joueurPlate-forme Console(s) :GameCubemodifier - modifier le code - modifier Wikidata Kidō Senshi Gundam: Senshitachi no Kiseki (機動...

Kevin Skinner

Kevin SkinnerNama lahirPatrick Kevin SkinnerLahir25 Februari 1974 (umur 49)McCracken County, Kentucky, Amerika SerikatAsalMayfield, Kentucky, Amerika SerikatGenreCountry, country rock, pop, rockPekerjaanPenyanyi, penulis lagi, petaniTahun aktif2009—sekarangLabelSYCO Music Patrick Kevin Skinner[1] (lahir 25 Februari 1974), atau lebih dikenal sebagai Kevin Skinner adalah pemenang America's Got Talent musim keempat. Referensi ^ Kentucky Birth Index, 1911-1999 kevin adalalah suatu ...

 

منارة برج البحري

منارة برج البحري   الموقع بلدية برج البحري، الجزائر إحداثيات 36°48′42″N 3°14′43″E / 36.81164°N 3.24531°E / 36.81164; 3.24531  ارتفاع بؤري 74 متر  نطاق المنارة 23 ميل بحري  صفات الضوء Fl(3) W 15s  رقم الأميرالية E6594  تعديل مصدري - تعديل   منارة برج البحري أو منارة رأس مافيتو ...

 

Strategi Solo vs Squad di Free Fire: Cara Menang Mudah!