Commit 258511a1 authored by Pierre Letouzey's avatar Pierre Letouzey
Browse files

seance 5

parent c4a0b3e6
Require Import List Arith.
Import ListNotations.
(** * Types dépendants, suite *)
(** Arbres binaires complets, via types inductifs *)
Inductive fulltree (A:Type) : nat -> Type :=
| FLeaf : A -> fulltree A 0
| FNode n : fulltree A n -> fulltree A n -> fulltree A (S n).
Arguments FLeaf {A}.
Arguments FNode {A} {n}.
Check FNode (FNode (FLeaf 1) (FLeaf 2)) (FNode (FLeaf 1) (FLeaf 2)).
(** Paires dépendantes *)
Print sigT.
Definition blist (A:Type) := list {n:nat & fulltree A n}.
Definition singleton {A} (a:A) : blist A := [ existT _ 0 (FLeaf a) ].
(** Le type [Fin] *)
Inductive Fin : nat -> Type :=
| Zero n : Fin (S n)
| Succ n : Fin n -> Fin (S n).
Arguments Zero {n}.
Arguments Succ {n}.
Check (Zero : Fin 1).
Fail Check (Succ Zero : Fin 1).
Check (Zero : Fin 2).
Check (Succ Zero : Fin 2).
(** Application: Vnth *)
Inductive vect (A:Type) : nat -> Type :=
| Vnil : vect A 0
| Vcons n : A -> vect A n -> vect A (S n).
Arguments Vnil {A}.
Arguments Vcons {A} {n}.
(* TODO
Fixpoint Vnth {A} {n} (p:Fin n) : vect A n -> A :=
match p in Fin m' return vect A m' -> A with
| @Zero m => fun (v:vect A (S m)) =>
match v with
| Vcons a _ => a
end
| @Succ m p => fun (v:vect A (S m)) =>
match v with
| Vcons _ v => Vnth v p
end
end.
*)
(** * Monades *)
(** ** Monade d'erreur *)
Definition head {A} (l:list A) : option A :=
match l with
| [] => None
| x :: _ => Some x
end.
Definition tail {A} (l:list A) : option (list A) :=
match l with
| [] => None
| _ :: l => Some l
end.
(** Exemple: la somme des deux premiers entiers d'une liste.
Evidemment, ça peut se faire de manière directe. *)
Definition somme_deux_premiers l :=
match l with
| a::b::_ => Some (a+b)
| _ => None
end.
(** Mais si maintenant on veut faire ça via des [head] et [tail],
c'est très lourd: *)
Definition somme_deux_premiers2 l :=
match tail l with
| None => None
| Some l' =>
match head l with
| None => None
| Some a =>
match head l' with
| Some b => Some (a+b)
| _ => None
end
end
end.
(** Un peu d'abstraction, via une fonction d'ordre supérieur *)
Definition option_map {A B} (o : option A)(f:A -> B) : option B :=
match o with
| Some x => Some (f x)
| None => None
end.
Definition somme_deux_premiers3 l :=
option_map (tail l)
(fun l' => option_map (head l)
(fun a => option_map (head l')
(fun b => a+b))).
Check somme_deux_premiers3. (* Pas le bon type !!! *)
(** Mieux: *)
Definition option_bind {A B} (o : option A) (f:A -> option B) : option B :=
match o with
| Some x => f x
| None => None
end.
Definition somme_deux_premiers4 l :=
option_bind (tail l)
(fun l' => option_bind (head l)
(fun a => option_bind (head l')
(fun b => Some (a+b)))).
Check somme_deux_premiers4.
Infix ">>=" := option_bind (at level 20, left associativity).
Definition somme_deux_premiers5 l :=
tail l >>= fun l' =>
head l >>= fun a =>
head l' >>= fun b =>
Some (a+b).
Compute somme_deux_premiers4 [1;2;3].
(** Généralisation : l'interface des monades *)
Module Type MONAD.
Parameter t : Type -> Type.
Parameter ret : forall {A}, A -> t A.
Parameter bind : forall {A B}, t A -> (A -> t B) -> t B.
End MONAD.
(** Les lois monadiques (qu'on garde ici implicites):
return a >>= f = f a
m >>= return = m
(m >>= f) >>= g = m >>= (fun x -> (f x >>= g))
*)
Module MErr <: MONAD.
Definition t := option.
Definition ret {A} := @Some A.
Definition bind {A B} := @option_bind A B.
End MErr.
Infix ">>=" := MErr.bind (at level 20, left associativity).
Definition somme_deux_premiers5 l :=
tail l >>= fun l' =>
head l >>= fun a =>
head l' >>= fun b =>
MErr.ret (a+b).
Inductive tree (A:Type) :=
| Leaf : A -> tree A
| Node : tree A -> tree A -> tree A.
Arguments Leaf {A}.
Arguments Node {A}.
(** Exemple, multiplication des feuilles d'un arbre, avec arrêt au premier zero *)
Fixpoint leafmul t :=
match t with
| Leaf n =>
if n =? 0 then None
else Some n
| Node g d =>
leafmul g >>= fun mulg =>
leafmul d >>= fun muld =>
Some (mulg * muld)
end.
Definition assert (b:bool) : option unit :=
if b then Some tt else None.
Fixpoint leafmul' t :=
match t with
| Leaf n =>
assert (negb (n =? 0)) >>= fun _ => Some n
| Node g d =>
leafmul' g >>= fun mulg =>
leafmul' d >>= fun muld =>
Some (mulg * muld)
end.
(** ** Monade de liste *)
Module MList <: MONAD.
Definition t := list.
Definition ret {A} (a:A) := [a].
Definition bind {A B} (l:list A) (f:A->list B) := List.flat_map f l.
End MList.
Infix ">>=" := MList.bind (at level 20, left associativity).
(** Exemple, produit cartésien *)
Definition cartprod {A} {B} (l:list A)(l' : list B) :=
l >>= fun a =>
l' >>= fun b =>
MList.ret (a,b).
Compute cartprod [1;2;3] [4;5].
Definition filter {A} (f : A -> bool) : list A -> list A := List.filter f.
(** ** Monade dtat *)
Module MState <: MONAD.
Definition t A := nat -> nat*A.
Definition ret {A} (a:A) := fun (st:nat) => (st,a).
Definition bind {A B} (m:t A) (f:A->t B) :=
fun st => let (st',a) := m st in f a st'.
End MState.
(** * Modules *)
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment