Seiten

Posts mit dem Label phantom type werden angezeigt. Alle Posts anzeigen
Posts mit dem Label phantom type werden angezeigt. Alle Posts anzeigen

Mittwoch, 21. Dezember 2011

F# Type Level Smart Constructor.

Es ist möglich, dank Phantom-Type und der Operatorenüberladung, die nummerische Prüfung bereits zur Kompilierungszeit durchzuführen.
Als Beispiel, wir wollen ausschlißlich den Widerstand von der Größe 2 oder 3 zulassen.
Der Funktionsparameter vom metalResistor-Smart Constructor wird in einen Phantom-Typ geändert. Da aber der Phantom-Typ-Konstruktor als privat deklariert ist, kann der Aufrufer an der metalResistor-Funktion nur einen von möglichen vordefinierten Werten - I,II,III,IV - übergeben.
//Resistor.fs
namespace SmartConstructors
open System
module Resistor  =
    
    type Bands = int

    type Resistor = private Metal of Bands | Ceramic of Bands with
        override x.ToString()= 
            match x with
            | (Metal v) -> "Metal " + v.ToString() 
            | (Ceramic v) -> "Ceramic " + v.ToString()

    type Zero = Zero

    type  Succ<'a> = private Succ of 'a with
        static member (|!|) (Zero, b:Succ<Succ<Zero>>) = Zero
        static member (|!|) (Zero, b:Succ<Succ<Succ<Zero>>>) = Zero |!| (Succ (Succ Zero))

    type Phantom<'a,'l> = private Phantom of 'a 

    let private nil : Phantom<int, Zero> = Phantom 0

    let inline private cons ((Phantom l ): Phantom<int,'l>) : Phantom<int, Succ<'l>> =
        Phantom (1 + l)

    let I = cons nil
    let II = cons (cons nil)
    let III = cons (cons (cons nil))
    let IV = cons (cons (cons (cons nil)))
    
    //run time check with assert.
    let metalResistor (Phantom b) =
        assert ( b >= 2 && b <= 3)
        Metal b

    let (|Metal|Ceramic|) n =
        match n with
        | (Metal v) -> Metal v
        | (Ceramic v) -> Ceramic v 
So weit, so gut, aber die Prüfung geschieht immer noch zur Laufzeit.
Jetzt kommt die Operatorenüberladung ins Spiel.
//compile time check.
    let inline typeLevelResistor (p : Phantom<int,'l>)  =
        Zero |!| (Unchecked.defaultof<'l>) |> ignore
        metalResistor p 

type Zero = | Zero
  type Succ<'a> =
    private | Succ of 'a
    with
      static member ( |!| ) : Zero:Zero * b:Succ<Succ<Zero>> -> Zero
      static member ( |!| ) : Zero:Zero * b:Succ<Succ<Succ<Zero>>> -> Zero
    end
  type Phantom<'a,'l> = private | Phantom of 'a
  val private nil : Phantom<int,Zero>
  val inline private cons : Phantom<int,'l> -> Phantom<int,Succ<'l>>
  val I : Phantom<int,Succ<Zero>>
  val II : Phantom<int,Succ<Succ<Zero>>>
  val III : Phantom<int,Succ<Succ<Succ<Zero>>>>
  val IV : Phantom<int,Succ<Succ<Succ<Succ<Zero>>>>>
  type Bands = int
  type Resistor =
    private | Metal of Bands
            | Ceramic of Bands
    with
      override ToString : unit -> string
    end
  val metalResistor : Phantom<int,'a> -> Resistor
  val inline typeLevelResistor :
    Phantom<int, ^l> -> Resistor
      when (Zero or  ^l) : (static member ( |!| ) : Zero *  ^l ->  ^a)
  val ( |Metal|Ceramic| ) : Resistor -> Choice<Bands,Bands>
Wenn man diesen Smart Constructor benutzt, wird die Prüfung zur Kompilierungszeit durchgeführt.

//Program.fs
open Resistor  
let resistor1 = metalResistor  II

let resistor2 = metalResistor  I

let typeLevelResistor1 = typeLevelResistor II
let typeLevelResistor2 = typeLevelResistor III

printfn "resistor1 %A" (resistor1.ToString())
printfn "resistor2 %A" (resistor2.ToString())

printfn "typeLevelResistor1 %A" (typeLevelResistor1.ToString())
printfn "typeLevelResistor2 %A" (typeLevelResistor2.ToString())

resistor1 "Metal 2" ---- DEBUGASSERTIONSFEHLER ----
---- Kurze Assertionsmeldung ----

---- Lange Assertionsmeldung ----


at Resistor.metalResistor(Phantom`2 _arg5) C:\Users\...\Documents\Visual Studio 2010\Projects\...\Resistor.fs(36)
at $Program.main@() C:\Users\...\Documents\Visual Studio 2010\Projects\...\TestSmart\Program.fs(6)
typeLevelResistor1 "Metal 2"
typeLevelResistor2 "Metal 3"

Zwar ist es nicht so schön wie in Haskell und die metalResistor-Funktion ist immer noch aufrufbar, aber immerhin.