TypeLevelNat

Description

Dieses Modul stellt die natuerlichen Zahlen (bei null beginnend) auf Typebene bereit. Diese nutzen wir fuer rudimentaere Typsicherheit im Umgang mit Matrizen.

Kernstueck sind die Typklasse ReifyNat und die Funktion reflectNat, die sich einem geeigneten Sinn zueinader invers verhalten -- es gilt folgende Spezifikation:

 reflectNat n reifyNat == n

fuer alle n >= 0. Siehe http://www.haskell.org/haskellwiki/Type_arithmetic.

Synopsis

Documentation

data Z

Darstellung der Null (Zero)

Instances

ReifyNat Z

data S n

Darstellung des Nachfolgers S n einer durch den Typ n dargestellen natuerlichen Zahl (Successor)

Instances

ReifyNat n ⇒ ReifyNat (S n)

type N0 = Z

Null

type N1 = S N0

Eins

type N2 = S N1

Zwei

type N3 = S N2

Drei

type N4 = S N3

Vier

class ReifyNat n where

Klasse, um natuerliche Zahlen der Typebene in Werte zu wandeln. Das Gegenstueck ist reflectNat.

Methods

reifyNat ∷ Proxy n → Nat

Gibt den zur Zahl n gehoerigen Wert zurueck.

Instances

ReifyNat Z
ReifyNat n ⇒ ReifyNat (S n)

reflectNat

Arguments

∷ Nat	die zu liftende natuerliche Zahl
→ (∀ n. ReifyNat n ⇒ Proxy n → r)	eine polymorphe Continuation, die Darstellungen aller Zahlen auf Typebene akzeptiert und ein Ergebnis vom Typ r produziert
→ r	das Endergebnis

Bringt eine auf Wertebene gegebene natuerliche Zahl aufs Typniveau.

reflectPositiveNat

Arguments

∷ Nat	die zu liftende positive Zahl
→ (∀ n. ReifyNat n ⇒ Proxy (S n) → r)	eine polymorphe Continuation, die Darstellungen aller positiven Zahlen auf Typebene akzeptiert und ein Ergebnis vom Typ r produziert
→ r	das Endergebnis

Bringt eine auf Wertebene gegebene positive natuerliche Zahl aufs Typniveau; auf Typebene hat man dann einen Typ der Form S n.

module Proxy

check_TypeLevelNat ∷ IO ()