{-# OPTIONS --no-positivity-check #-} module L6 where ---------------------------------------------------------------------- -- Lecture 6 : Holes in Data ---------------------------------------------------------------------- -- We'll need a lot of the stuff from lecture 5. data Zero : Set where data One : Set where void : One data Two : Set where left : Two right : Two data Sigma (S : Set)(T : S -> Set) : Set where _,_ : (s : S)(t : T s) -> Sigma S T infixr 40 _,_ _*_ : Set -> Set -> Set S * T = Sigma S \ s -> T data _:+:_ (S T : Set) : Set where inl : S -> S :+: T inr : T -> S :+: T data Description : Set1 where -- that's a set of sets! DSigma : (S : Set) -> (S -> Description) -> Description DPlace : Description _D*_ : Description -> Description -> Description D1 : Description infixr 40 _D*_ _D+_ : Description -> Description -> Description S D+ T = DSigma Two Args where Args : Two -> Description Args left = S Args right = T infixr 30 _D+_ NAT : Description NAT = D1 D+ DPlace TREE : Description TREE = D1 D+ DPlace D* DPlace LIST : Set -> Description LIST X = D1 D+ DSigma X \ _ -> DPlace D0 : Description D0 = DSigma Zero Args where Args : Zero -> Description Args () _!_ : Description -> Set -> Set DSigma S D ! X = Sigma S (\ s -> D s ! X ) DPlace ! X = X (S D* T) ! X = (S ! X) * (T ! X) D1 ! X = One data Data (D : Description) : Set where [_] : D ! Data D -> Data D traverse : (F : Set -> Set) (pure : {X : Set} -> X -> F X) (_$_ : {S T : Set} -> F (S -> T) -> F S -> F T) (D : Description) {S T : Set} -> (S -> F T) -> D ! S -> F (D ! T) traverse F pure _$_ D {S}{T} f = tr D where tr : (D : Description) -> D ! S -> F (D ! T) tr (DSigma S D) (s , d) = pure (_,_ s) $ tr (D s) d tr DPlace d = f d tr (S D* T) (s , t) = (pure _,_ $ tr S s) $ tr T t tr D1 d = pure void map : (D : Description){A B : Set} -> (A -> B) -> D ! A -> D ! B map (DSigma S D) f (s , d) = s , map (D s) f d map DPlace f a = f a map (S D* T) f (s , t) = map S f s , map T f t map D1 f d = d mapFold : (R D : Description){T : Set} -> (R ! T -> T) -> D ! Data R -> D ! T mapFold R (DSigma S D) f (s , d) = s , mapFold R (D s) f d mapFold R DPlace f [ r ] = f (mapFold R R f r) mapFold R (S D* T) f (s , t) = mapFold R S f s , mapFold R T f t mapFold R D1 f void = void fold : {R : Description}{T : Set} -> (R ! T -> T) -> Data R -> T fold {R} f [ r ] = f (mapFold R R f r) ------------------------------------------------------------- Diff : Description -> Description Diff (DSigma S D) = DSigma S \ s -> Diff (D s) Diff DPlace = D1 Diff (S D* T) = Diff S D* T D+ S D* Diff T Diff D1 = D0 Focus : Description -> Description Focus D = Diff D D* DPlace layer : (D : Description){X : Set} -> Focus D ! X -> D ! X layer (DSigma S D) ((s , d) , x) = s , layer (D s) (d , x) layer DPlace (c , x) = x layer (S D* T) ((left , s' , t) , x) = layer S (s' , x) , t layer (S D* T) ((right , s , t') , x) = s , layer T (t' , x) layer D1 ((() , _) , x) plug : (D : Description) -> Data D -> Data (LIST (Diff D ! Data D)) -> Data D plug D t [ left , void ] = t plug D t [ right , d' , d's ] = plug D [ layer D (d' , t) ] d's ---------------------------------------------------------- data Maybe (X : Set) : Set where just : X -> Maybe X nothing : Maybe X data AllOrNothing (D : Description)(X : Set) : D ! Maybe X -> Set where allJust : (dx : D ! X) -> AllOrNothing D X (map D just dx) someNothing : (d' : Diff D ! Maybe X) -> AllOrNothing D X (layer D (d' , nothing)) allOrNothing : (D : Description)(X : Set)(dmx : D ! Maybe X) -> AllOrNothing D X dmx allOrNothing (DSigma S D) X (s , dmx) with allOrNothing (D s) X dmx allOrNothing (DSigma S D) X (s , .(map (D s) just dx)) | allJust dx = allJust (s , dx) allOrNothing (DSigma S D) X (s , .(layer (D s) (d' , nothing))) | someNothing d' = someNothing (s , d' ) allOrNothing DPlace X (just x) = allJust x allOrNothing DPlace X nothing = someNothing void allOrNothing (S D* T) X dmx = {! !} allOrNothing D1 X dmx = allJust dmx tryAllJust : (D : Description)(X : Set)(dmx : D ! Maybe X) -> Maybe (D ! X) tryAllJust D X dmx with allOrNothing D X dmx tryAllJust D X .(map D just dx) | allJust dx = just dx tryAllJust D X .(layer D (d' , nothing)) | someNothing d' = nothing