search

ct-gradual-typing / Papers

The Combination of Dynamic and Static Typing from a Categorical Perspective
10 stars 0 forks source link

Question for meeting #22

Closed michaelto20 closed 7 years ago

michaelto20 commented 7 years ago

  1. Should data Prog = Def Vnm Type Term be data Prog = Vnm Type Term For example, from out test file: 

     true : ? -> ? -> ?
 true = \(p:?).\(q:?).p

    Would Vnm be true, Type be ? -> ? -> ?, and Term be \(p:?).\(q:?).p? If this is correct, what would Def be?

heades commented 7 years ago

I think you are misunderstanding what Def Vnm Type Term means. The Def is the name of the constructor and not an argument. For example, a valid definition can be defined by Def (s2n "x") Unit Triv. The Def is simply the name we use to indicate that we have a definition.

Your example above would be defined as Def (s2n "true") (Arr U (Arr U U)) (Lam (Lam b)) where Lam (Lam b) is pseudocode for the lambda-abstraction.

Does this make sense?