依值型別編程 / Dependently Typed Programming

• 講者: 穆信成 Shin-Cheng Mu

• Introduction — Why Dependent Types?
• Syntax, Functions, Values, and Simple Usage of Dependent Types.
  • 1-Intro.agda (completed: 1-IntroC.agda).
  • 2-DepTypes.agda (completed: 2-DepTypesC.agda).
• Inductive Family.
  • 3-Vectors.agda (completed: 3-VectorsC.agda).
• Example: Binomial Heaps
  • 4-BinomialHeap.agda (completed: 4-BinomialHeapC.agda).
  • See also the slides by Josh Ko.

If you happened to have an earlier version of Agda installed, you may need to put the following derivatives into your program file:

{-# BUILTIN ZERO zero  #-}
{-# BUILTIN SUC  suc   #-}

infixl 6 _⊔_
postulate
  Level : Set
  lzero  : Level
  lsuc   : Level → Level
  _⊔_   : Level → Level → Level

{-# BUILTIN LEVEL     Level #-}
{-# BUILTIN LEVELZERO lzero  #-}
{-# BUILTIN LEVELSUC  lsuc   #-}
{-# BUILTIN LEVELMAX  _⊔_   #-}