{
  localUrl: '../page/prog_dep_typ.html',
  arbitalUrl: 'https://arbital.com/p/prog_dep_typ',
  rawJsonUrl: '../raw/3t7.json',
  likeableId: '2556',
  likeableType: 'page',
  myLikeValue: '0',
  likeCount: '1',
  dislikeCount: '0',
  likeScore: '1',
  individualLikes: [
    'EricRogstad'
  ],
  pageId: 'prog_dep_typ',
  edit: '2',
  editSummary: '',
  prevEdit: '1',
  currentEdit: '2',
  wasPublished: 'true',
  type: 'wiki',
  title: 'Programming in  Dependent Type Theory',
  clickbait: 'Working with simple types in Lean',
  textLength: '4631',
  alias: 'prog_dep_typ',
  externalUrl: '',
  sortChildrenBy: 'likes',
  hasVote: 'false',
  voteType: '',
  votesAnonymous: 'false',
  editCreatorId: 'JackGallagher',
  editCreatedAt: '2016-05-26 05:21:54',
  pageCreatorId: 'JackGallagher',
  pageCreatedAt: '2016-05-26 05:16:46',
  seeDomainId: '0',
  editDomainId: 'AlexeiAndreev',
  submitToDomainId: '0',
  isAutosave: 'false',
  isSnapshot: 'false',
  isLiveEdit: 'true',
  isMinorEdit: 'false',
  indirectTeacher: 'false',
  todoCount: '0',
  isEditorComment: 'false',
  isApprovedComment: 'true',
  isResolved: 'false',
  snapshotText: '',
  anchorContext: '',
  anchorText: '',
  anchorOffset: '0',
  mergedInto: '',
  isDeleted: 'false',
  viewCount: '75',
  text: 'All code in this article was written in the Lean theorem prover, which means you can copy any of it and paste it [here](https://leanprover.github.io/tutorial/?live) to try it out.\n\n## Arithmetic and Interaction\nWhile Lean is nominally an interactive theorem prover, much of the power of type theory comes from the fact that you can treat it like a programming language.\n\nThere are a few different commands for interacting with Lean.\nThe one I make the most use of is the `check` command, which prints out the type of the expression following it.\nSo, for example, `check 3` outputs `num`, and `check (3 : nat)` outputs `nat`.\n\nWe can also make definitions\n\n    definition five : num := 3 + 2\n\nThis declares a new constant `five` of type `num` to which we give the value `3 + 2`.\nWe can define functions with similar syntax\n\n    definition num.const₀ : num → num → num := λ x y, x -- this is a comment\n    -- Lean can infer types whenever they're unique\n    definition num.const₁                    := λ (x y : num), x\n    -- we can also name the arguments in the definition rather than the function body\n    definition num.const₂ (x y : num)        := x\n\nThe definition of polymorphic functions becomes the first point where we get a hint about what makes programming in dependent type theory different from, say, Haskell.\nIn dependent type theory, the term and type languages are unified, so in order to write a polymorphic function we must take the type as an argument.\n\n    definition poly_id (A : Type) := λ (a : A), a\n    -- or, equivalently\n    definition poly_id₁ := λ A (a : A), a\n    -- applied to arguments\n    check poly_id num 1 -- num\n    check poly_id (num → num → num) num.const -- num → num → num\n\nExercise: write a polymorphic version of `num.const₀`.\n\n%%hidden(Show solution):\n    definition poly_const (A B : Type) (a : A) (b : B) := a\n%%\n\nHaving to explicitly indicate types everywhere is a pain.\nIn order to get around that, most proof assistants provide support for implicit arguments, which let you leave out arguments that only have one valid value.\nIn Lean, the syntax for implicits looks like this:\n\n    definition id {A : Type} := λ (a : A), a\n\n## Inductive types ##\nOf course, none of this would be that useful if we couldn't define *new* types.\nThere are lots of ways to craft new types in dependent type theory, but among the most fundamental is the creation of inductive types.\n\nTo define a new inductive type, you give a list of constructor tags, each associated with a type representing the arguments it takes.\nThe simplest ones are just enumerations. For example, the days of the week:\n\n    inductive weekday : Type :=\n    | mon : weekday\n    | tue : weekday\n    | wed : weekday\n    | thu : weekday\n    | fri : weekday\n    | sat : weekday\n    | sun : weekday\n\nThis creates a new type `weekday`, and seven new constants (`weekday.mon`, `weekday.tue`, `weekday.wed`...) of type `weekday`.\nIf you're familiar with Haskell, you'll correctly notice that this looks an awful lot like GADT declarations.\n\nJust like in Haskell, we can parametrize our types over other types, making new types like `either`:\n\n    inductive either (A B : Type) : Type :=\n    | inl {} : A → either A B``\n    | inr {} : B → either A B\n\nFrom this declaration, we get a new constant `either : Type → Type → Type`.\nThis represents the union of the types `A` and `B`, the type of values that belong either to `A` or `B`.\n\nWe can also define recursive types, such as natural numbers\n\n    inductive nat : Type :=\n    | zero : nat\n    | succ : nat → nat\n\nThe easiest way to define functions over `nat`s is recursively.\nFor example, we can define addition as\n\n    definition add (n : nat) : nat -> nat\n    | nat.zero := n\n    | (nat.succ m) := nat.succ (add m) -- n is constant at every recursive call\n\nBringing both of these together we can define the type of linked lists\n\n    inductive list (A : Type) : Type := \n    | nil {} : list A\n    | cons : A → list A → list A\n\nWe can also define functions over lists by pattern matching\n\n    definition map {A B : Type} (f : A → B) : list A → list B\n    | list.nil := list.nil\n    | (list.cons x xs) := list.cons (f x) (map xs) -- f is constant at every recursive call\n\nExercise: write `foldr` and `foldl` by pattern matching\n\n%%hidden(Show solution):\n    definition foldr {A B : Type} (r : A → B → B) (vnil : B) : list A → B\n    | list.nil := vnil\n    | (list.cons x xs) := r x (foldr xs)\n\n    definition foldl {A B : Type} (r : B → A → B) : B → list A → B :=\n    | b list.nil := b\n    | b (list.cons x xs) := foldl (r b x) xs\n%%\n',
  metaText: '',
  isTextLoaded: 'true',
  isSubscribedToDiscussion: 'false',
  isSubscribedToUser: 'false',
  isSubscribedAsMaintainer: 'false',
  discussionSubscriberCount: '1',
  maintainerCount: '1',
  userSubscriberCount: '0',
  lastVisit: '',
  hasDraft: 'false',
  votes: [],
  voteSummary: 'null',
  muVoteSummary: '0',
  voteScaling: '0',
  currentUserVote: '-2',
  voteCount: '0',
  lockedVoteType: '',
  maxEditEver: '0',
  redLinkCount: '0',
  lockedBy: '',
  lockedUntil: '',
  nextPageId: '',
  prevPageId: '',
  usedAsMastery: 'false',
  proposalEditNum: '0',
  permissions: {
    edit: {
      has: 'false',
      reason: 'You don't have domain permission to edit this page'
    },
    proposeEdit: {
      has: 'true',
      reason: ''
    },
    delete: {
      has: 'false',
      reason: 'You don't have domain permission to delete this page'
    },
    comment: {
      has: 'false',
      reason: 'You can't comment in this domain because you are not a member'
    },
    proposeComment: {
      has: 'true',
      reason: ''
    }
  },
  summaries: {},
  creatorIds: [
    'JackGallagher'
  ],
  childIds: [],
  parentIds: [
    'type_theory'
  ],
  commentIds: [],
  questionIds: [],
  tagIds: [
    'type_theory',
    'work_in_progress_meta_tag'
  ],
  relatedIds: [],
  markIds: [],
  explanations: [],
  learnMore: [],
  requirements: [],
  subjects: [],
  lenses: [],
  lensParentId: '',
  pathPages: [],
  learnMoreTaughtMap: {},
  learnMoreCoveredMap: {},
  learnMoreRequiredMap: {},
  editHistory: {},
  domainSubmissions: {},
  answers: [],
  answerCount: '0',
  commentCount: '0',
  newCommentCount: '0',
  linkedMarkCount: '0',
  changeLogs: [
    {
      likeableId: '0',
      likeableType: 'changeLog',
      myLikeValue: '0',
      likeCount: '0',
      dislikeCount: '0',
      likeScore: '0',
      individualLikes: [],
      id: '11081',
      pageId: 'prog_dep_typ',
      userId: 'JackGallagher',
      edit: '2',
      type: 'newEdit',
      createdAt: '2016-05-26 05:21:54',
      auxPageId: '',
      oldSettingsValue: '',
      newSettingsValue: ''
    },
    {
      likeableId: '0',
      likeableType: 'changeLog',
      myLikeValue: '0',
      likeCount: '0',
      dislikeCount: '0',
      likeScore: '0',
      individualLikes: [],
      id: '11079',
      pageId: 'prog_dep_typ',
      userId: 'JackGallagher',
      edit: '0',
      type: 'deleteTeacher',
      createdAt: '2016-05-26 05:17:03',
      auxPageId: 'prog_dep_typ',
      oldSettingsValue: '',
      newSettingsValue: ''
    },
    {
      likeableId: '0',
      likeableType: 'changeLog',
      myLikeValue: '0',
      likeCount: '0',
      dislikeCount: '0',
      likeScore: '0',
      individualLikes: [],
      id: '11080',
      pageId: 'prog_dep_typ',
      userId: 'JackGallagher',
      edit: '0',
      type: 'deleteSubject',
      createdAt: '2016-05-26 05:17:03',
      auxPageId: 'prog_dep_typ',
      oldSettingsValue: '',
      newSettingsValue: ''
    },
    {
      likeableId: '0',
      likeableType: 'changeLog',
      myLikeValue: '0',
      likeCount: '0',
      dislikeCount: '0',
      likeScore: '0',
      individualLikes: [],
      id: '11074',
      pageId: 'prog_dep_typ',
      userId: 'JackGallagher',
      edit: '0',
      type: 'newTeacher',
      createdAt: '2016-05-26 05:16:46',
      auxPageId: 'prog_dep_typ',
      oldSettingsValue: '',
      newSettingsValue: ''
    },
    {
      likeableId: '0',
      likeableType: 'changeLog',
      myLikeValue: '0',
      likeCount: '0',
      dislikeCount: '0',
      likeScore: '0',
      individualLikes: [],
      id: '11077',
      pageId: 'prog_dep_typ',
      userId: 'JackGallagher',
      edit: '0',
      type: 'newSubject',
      createdAt: '2016-05-26 05:16:46',
      auxPageId: 'prog_dep_typ',
      oldSettingsValue: '',
      newSettingsValue: ''
    },
    {
      likeableId: '0',
      likeableType: 'changeLog',
      myLikeValue: '0',
      likeCount: '0',
      dislikeCount: '0',
      likeScore: '0',
      individualLikes: [],
      id: '11078',
      pageId: 'prog_dep_typ',
      userId: 'JackGallagher',
      edit: '1',
      type: 'newEdit',
      createdAt: '2016-05-26 05:16:46',
      auxPageId: '',
      oldSettingsValue: '',
      newSettingsValue: ''
    },
    {
      likeableId: '0',
      likeableType: 'changeLog',
      myLikeValue: '0',
      likeCount: '0',
      dislikeCount: '0',
      likeScore: '0',
      individualLikes: [],
      id: '10996',
      pageId: 'prog_dep_typ',
      userId: 'JackGallagher',
      edit: '1',
      type: 'newTag',
      createdAt: '2016-05-25 21:50:05',
      auxPageId: 'type_theory',
      oldSettingsValue: '',
      newSettingsValue: ''
    },
    {
      likeableId: '0',
      likeableType: 'changeLog',
      myLikeValue: '0',
      likeCount: '0',
      dislikeCount: '0',
      likeScore: '0',
      individualLikes: [],
      id: '10995',
      pageId: 'prog_dep_typ',
      userId: 'JackGallagher',
      edit: '1',
      type: 'newTag',
      createdAt: '2016-05-25 21:50:00',
      auxPageId: 'work_in_progress_meta_tag',
      oldSettingsValue: '',
      newSettingsValue: ''
    },
    {
      likeableId: '0',
      likeableType: 'changeLog',
      myLikeValue: '0',
      likeCount: '0',
      dislikeCount: '0',
      likeScore: '0',
      individualLikes: [],
      id: '10951',
      pageId: 'prog_dep_typ',
      userId: 'JackGallagher',
      edit: '1',
      type: 'newParent',
      createdAt: '2016-05-25 21:07:48',
      auxPageId: 'type_theory',
      oldSettingsValue: '',
      newSettingsValue: ''
    }
  ],
  feedSubmissions: [],
  searchStrings: {},
  hasChildren: 'false',
  hasParents: 'true',
  redAliases: {},
  improvementTagIds: [],
  nonMetaTagIds: [],
  todos: [],
  slowDownMap: 'null',
  speedUpMap: 'null',
  arcPageIds: 'null',
  contentRequests: {}
}