Skip to content

Latest commit

 

History

History
458 lines (353 loc) · 7.49 KB

slides.md

File metadata and controls

458 lines (353 loc) · 7.49 KB
Raw
marp title author theme paginate math style
true
Generalized Algebraic Data Types in OCaml
Marius Weidner
uncover
true
katex
:root { font-family: 'JetBrains Mono', serif !important; font-variant-ligatures: common-ligatures; } code { font-family: 'JetBrains Mono', serif !important; font-variant-ligatures: common-ligatures; border-radius: 12px; } pre { font-size: 1rem; border-radius: 12px; } p { font-family: 'JetBrains Mono', serif !important; font-variant-ligatures: common-ligatures; } section::after { background: none } .columns { display: grid; grid-template-columns: repeat(2, minmax(0, 1fr)); gap: 0.75rem; } .subtitle { font-size: 0.7rem; letter-spacing: 0.00000001rem; } footer { color: black; }

Generalized Algebraic Data Types

in OCaml

Sprachdefinition

$$ \begin{align*}

Expr ::=& \text{ } \text{ true} \text{ } \&| \text{ } \text{false} \text{ } \&| \text{ } -^?0..9^+ \&| \textbf{ if } Expr \textbf{ then } Expr \textbf{ else } Expr \end{align*} $$

<style scoped> pre { font-size: 0.8rem; } div.error > pre { font-size: 0.777rem; border: 0.05rem; background-color: rgb(242, 241, 244); border-color: #B00020; border-style: solid; border-radius: 12px; } </style>

Gültige Programme

true                     
if true then 42 else 0   
if true then 
  if true then 42 else 0 
else 
  0

Ungültige Programme

if true then 0
if 0 then true else false
if true then 
  if true then 42 else 0
else
  false

In einer Welt ohne GADTs

<style scoped> pre { font-size: 1rem; } </style> 
type expr =
  | Bool of bool
  | Int  of int
  | If   of expr * expr * expr

Syntaxbaum ohne GADTs

let rec eval : expr -> expr = function
  | If (c, t, e) -> begin match eval c with
      | Bool true  -> eval t
      | Bool false -> eval e
      | _ -> failwith "need bool!"
    end
  | e -> e

Evaluationsfunktion ohne GADTs

<style scoped> pre { font-size: 0.7rem; } </style> 
eval (If 
     (Bool true,
     (Int 42),
     (Int 0)))
- : expr = Int 42
eval (If 
     (Int 42,
     (Bool false),
     (Int 0)))                  
Exception: Failure "need bool!"

Beispiele ohne GADTs

  • Ungültige Programmdefinitionen
  • Laufzeitfehler im Interpreter
  • Zweige mit verschiedenen Typen

In einer Welt mit GADTs

<style scoped> pre { font-size: 0.9rem; } </style> 
type _ expr =
  | Bool : bool -> bool expr
  | Int  : int  -> int  expr
  | If   : bool expr * 'a expr * 'a expr -> 'a expr

Syntaxbaum mit GADTs

<style scoped> pre { font-size: 0.85rem; } </style> 
let rec eval : .. = function
  | Bool b        -> b
  | Int i         -> i
  | If (c, t, e)  -> if eval c then eval t else eval e

Evaluationsfunktion mit GADTs

<style scoped> pre { font-size: 0.8rem; } div.error > pre { font-size: 0.77rem; border: 0.1rem; background-color: rgb(242, 241, 244); border-color: #B00020; border-style: solid; border-radius: 12px; } </style> 
eval (If 
     (Int 42,
     (Bool true),
     (Bool false)))
eval (If 
     (Bool true,
     (Bool false),
     (Int 42)))
Error: Type int is not compatible with type bool

Beispiele mit GADTs

  • Nur gültige Programmdefinitionen
  • Keine Laufzeitfehler im Interpreter
  • Exhaustive Patternmatching

Locally Abstract Types

<style scoped> pre { font-size: 0.85rem; border: 0.1rem; border-color: #B00020; border-style: solid; border-radius: 12px; } </style> 
let rec eval (type a) (e : a expr) : a = match e with
  | Bool b -> b
  | Int i  -> i
  | If (c, t, e)  -> if eval c then eval t else eval e
Error: This expression has type a expr but an
       expression was expected of type bool expr

Evaluationsfunktion mit GADTs

Polymorphic Recursion

<style scoped> pre { font-size: 0.75rem; } </style> 
let rec eval : 'a. 'a expr -> 'a = 
    fun (type a) (e : a expr) : a -> match e with
      | Bool b -> b
      | Int i  -> i
      | If (c, t, e)  -> if eval c then eval t else eval e

Evaluationsfunktion mit GADTs

Syntactic Sugar

<style scoped> pre { font-size: 0.8rem; } </style> 
let rec eval : type a. a expr -> a = function
  | Bool b -> b
  | Int i  -> i
  | If (c, t, e)  -> if eval c then eval t else eval e

Evaluationsfunktion mit GADTs

Existential Types

type stringable =                          
  Stringable : { 
    item: 'a; 
    to_string: 'a -> string 
  } -> stringable
let print (Stringable s) = 
  print_endline (s.to_string s.item)

Vertiefendes Beispiel

<style scoped> pre { font-size: 0.75rem; } </style> 
type (_, _) mode = 
  | Unsafe : ('a, 'a) mode
  | Option : ('a, 'a option) mode                  
let first : type a r. a list -> (a, r) mode -> r = 
  fun lst mde -> match lst with
    | hd :: tl -> (match mde with
      | Unsafe -> hd
      | Option -> Some hd)
    | [ ] -> (match mde with
      | Unsafe -> failwith "list is empty"
      | Option -> None)

Limitationen

  • Typinferenz unentscheidbar $\rightarrow$ Typannotationen notwendig

  • |-Patterns nicht auflösbar $\rightarrow$ Manuell auflösen und Logik auslagern

  • [@@-deriving ..]-Annotation nicht möglich $\rightarrow$ Non-GADT Version benötigt

Zusammengefasst

  • GADTs erlauben Konstrukturen verschiedene Typparameter einzusetzen
  • Stärkere Aussagen auf Typebene möglich
  • Patternmatching nutzt die zusätzlichen Informationen
  • GATDs erlauben existenziell quantifizierte Typen zu formen
  • Typinferenz wird unentscheidbar

Folien & Code

github.com/Mari-W/ocaml-gadts

Literatur