Why dependent types matter

被引:9
|
作者
McKinna, J [1 ]
机构
[1] Univ St Andrews, St Andrews KY16 9AJ, Fife, Scotland
关键词
algorithms; design; languages; theory; verification;
D O I
10.1145/1111320.1111038
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
Language designers have in recent years proposed a wealth of richer type systems for programming which seek to extend the range of statically enforced guarantees on data and code. Most such proposals have been evolutionary extensions of ML or Haskell, offering programmers a balanced compromise between expressive strength and existing well-understood technology. Typically they revolve around type- or kind-indexed types such as GADTs, supported by limited equality reasoning at the type-checking level, thus separating the dynamic behaviour of programs from the (simpler) static behaviour of indexing information occurring in their types. I want to argue in this talk for a more radical departure from such practice by examining full spectrum type dependency, lifting such restrictions on the data upon which types may depend. Conor McBride and I designed the language EPIGRAM for experiments in programming with inductive families of data (of which GADTs are a special case). Using it for illustration, I will explore some of the possibilities and challenges afforded by full spectrum type dependency at the static and dynamic level: types directly support modelling complex invariants in terms of other data (rather than their types), with a Curry-Howard flavour of data-as-evidence; such complexity is on a 'pay-as-you-go' basis, while keeping type annotations and other syntactic overheads to a minimum; data decomposition steps, e.g. case analysis, furnish more informative interactions between types and values during typechecking; such steps may moreover be abstractly specified by their types, and thus user definable; this supports a style of programming embracing "learning by testing', views, and Burstall's 'hand simulation plus a little induction'; the absence of a rigid phase distinction need not lead to type-passing or excessive run-time overhead; effectful computation, in particular partiality, can be incorporated via variations on existing ideas such as monads. This talk is based on joint work with Conor McBride, Edwin Brady and Thorsten Altenkirch.
引用
收藏
页码:1 / 1
页数:1
相关论文
共 50 条
  • [21] Why DLMs matter
    Shank, J
    LIBRARY JOURNAL, 2005, : 16 - +
  • [22] Why Stories Matter
    Robinson, Brian
    SCIENTIST, 2009, 23 (12): : 14 - 14
  • [23] Why Families Matter
    Lindemann, Hilde
    PEDIATRICS, 2014, 134 : S97 - S103
  • [24] Why economics matter
    不详
    EUROPEAN JOURNAL OF CANCER, 2003, 39 (05) : 555 - 555
  • [25] Why unions matter
    Le Blanc, P
    LABOUR-LE TRAVAIL, 1999, (44): : 279 - 281
  • [26] Why interfaces matter
    Schlack, M
    BYTE, 1997, 22 (07): : 12 - 12
  • [27] Why the Romantics Matter
    Wang, Orrin N. C.
    CRITICAL INQUIRY, 2016, 42 (04) : 1005 - 1006
  • [28] Why the arts matter
    Axelrod, Paul
    PHYSICS WORLD, 2018, 31 (01) : 17 - 18
  • [29] Why Matter Matters
    Ferraris, Maurizio
    PHILOSOPHICAL READINGS, 2014, 6 (02): : 4 - +
  • [30] Why Languages Matter
    Yelick, Katherine
    2018 IEEE INTERNATIONAL PARALLEL AND DISTRIBUTED PROCESSING SYMPOSIUM WORKSHOPS (IPDPSW 2018), 2018, : 895 - 895