8Ī useful generic function is compress which compresses data to string of bits. ☞ An element rt of type Type τ is a representation of τ. RInt RChar RList (Type α) RPair (Type α) (Type β) Basic idea: define a data type whose elements represent types. Generic functions We can use phantom types to implement generic functions, functions that work for a family of types. Since the type argument of Term is not related to any component, we call Term a phantom type. I The type Term β might not even be inhabited: there are, for instance, no terms of type Term String. I We cannot define a mapping function (α → β) → (Term α → Term β) as for many other data types. I Term is not a container type: an element of Term Int is an expression that evaluates to an integer it is not a data structure that contains integers. Maini let one = Succ Zero Maini : type one Term Int Maini eval one 1 Maini eval (IsZero one) False Maini IsZero (IsZero one) Type error: couldn’t match ‘Int’ against ‘Bool’ Introducing phantom types-continued Here is a short interactive session that shows the interpreter in action. If it receives a Boolean expression, then it returns a Boolean. ☞ The interpreter is quite noticeable in that it is tag free. Term τ → τ, each equation has a more specific type as dictated by the type constraints. Term τ → τ 0 eval e + 1 eval e − 1 eval e 0 if eval e1 then eval e2 else eval e3Įven though eval is assigned the type ∀τ. Its definition proceeds by straightforward structural recursion. Introducing phantom types-continued Here is a simple interpreter for the expression language. The type variable α does not appear on the left-hand side it can be seen as being existentially quantified. Thus, Zero has Type τ with the additional constraint τ = Int. Zero Succ (Term Int) Pred (Term Int) IsZero (Term Int) If (Term Bool ) (Term α) (Term α)
Idea: augment the data construct by type equations that allow us to constrain the type argument of Term. Term Bool → Term α → Term α → Term αĪlas, the signature above cannot be translated into a data declaration. Term Int Term Int → Term Int Term Int → Term Bool ∀α. Idea: parameterize the Term type so that Term τ comprises only terms of type τ. ☞ This rules out a simple Term data type as this choice would allow us to freely mix terms of different types. You are a firm believer of static typing, so you would like your embedded language to be statically typed, as well. Introducing phantom types Suppose you want to embed a simple expression language in Haskell. ‘Maini ’ is the prompt ‘: type’ displays the type of an expression. Maini : type format (Lit "Richard") String Maini format (Lit "Richard") "Richard" Maini : type format Int Int → String Maini format Int 60 "60" Maini : type format (String :^: Lit " is " :^: Int) String → Int → String Maini format (String :^: Lit " is " :^: Int) "Richard" 60 "Richard is 60" NB. ~ralf/talks.html#T35.)Ī puzzle: C’s printf in Haskell Here is a session that illustrates the puzzle-we renamed printf to format. Fun with Phantom Types RALF HINZE Institut f¨ur Informatik III, Universit¨at Bonn R¨omerstraße 164, 53117 Bonn, Germany Email: Homepage: March, 2003 (Pick the slides at.
0 kommentar(er)
