Go backward to Generic Element Types Go up to Top Go forward to Another Example

Hiding the Representation

type GenericStack =
   forall Item. exists Stack. GenericStackWRT[Item][Stack]

type GenericStackWRT[Item][Stack] =
  {emptyStack: List[Item],
   push: (Item x List[Item]) -> List[Item]
   pop: List[Item] x List[Item],
   top: List[Item] -> Item}

value listStackPackage: GenericStack =
   all[Item]
      pack[Stack = List[Item]
         in GenericStackWRT[Item][Stack]]
      genericListStack[Item]
value useStack =
   fun(stackPackage: GenericStack)
      open stackPackage[Int] as p[stackRep]
      in p.top(p.push(3, p.emptystack))

useStack(listStackPackage)