Serguey Zefirov (thesz) wrote,
Serguey Zefirov
thesz

О, сколько нам открытий чудных!

Почти насобачился.

------------------------------------------------------------------------------
     (   X : *    !                            ( x : X ;  xs : List X !
data !------------!  where (--------------! ;  !----------------------!
     ! List X : * )        ! nil : List X )    !  cons x xs : List X  )
------------------------------------------------------------------------------
     ( X : * ;  Y : * ;  f : all x : X => Y ;  xs : List X !
let  !-----------------------------------------------------!
     !                  map f xs : List Y                  )
                                                            
     map f xs <= rec xs                                     
     { map f xs <= case xs                                  
       { map f nil => nil                                   
         map f (cons x xs) => cons (f x) (map f xs)         
       }                                                    
     }                                                      
------------------------------------------------------------------------------
     ( A : *                                                             !
     !                                                                   !
     ! B : * ;  f : all a : A => all b : B => A ;  a0 : A ;  bs : List B !
let  !-------------------------------------------------------------------!
     !                         foldl f a0 bs : A                         )
                                                                          
     foldl f a0 bs <= rec bs                                              
     { foldl f a0 bs <= case bs                                           
       { foldl f a0 nil => a0                                             
         foldl f a0 (cons b bs) => foldl f (f a0 b) bs                    
       }                                                                  
     }                                                                    
------------------------------------------------------------------------------
                                          (   x : Nat    !
data (---------!  where (------------! ;  !--------------!
     ! Nat : * )        ! zero : Nat )    ! succ x : Nat )
------------------------------------------------------------------------------
     (   x, y : Nat   !                    
let  !----------------!                    
     ! plus x y : Nat )                    
                                           
     plus x y <= rec x                     
     { plus x y <= case x                  
       { plus zero y => y                  
         plus (succ x) y => succ (plus x y)
       }                                   
     }                                     
------------------------------------------------------------------------------
inspect plus (succ zero) (succ zero) => succ (succ zero) : Nat
------------------------------------------------------------------------------
inspect map succ (cons zero (cons (succ zero) nil))                   
          => cons (succ zero) (cons (succ (succ zero)) nil) : List Nat
------------------------------------------------------------------------------
inspect map (lam x => foldl plus (succ zero) (cons x nil))                    
        % (cons zero (cons (succ zero) (cons (succ (succ zero)) nil)))        
          => cons (succ  ! (cons (succ (succ zero))               ! : List Nat
                  !% zero) !% (cons (succ (succ (succ zero))) nil))           
------------------------------------------------------------------------------
     (  a, b : Nat   !                     
let  !---------------!                     
     ! mul a b : Nat )                     
                                           
     mul a b <= rec a                      
     { mul a b <= case a                   
       { mul zero b => zero                
         mul (succ a) b => plus b (mul a b)
       }                                   
     }                                     
------------------------------------------------------------------------------
     (        a : Nat        !                          
let  !-----------------------!                          
     ! generate a : List Nat )                          
                                                        
     generate a <= rec a                                
     { generate a <= case a                             
       { generate zero => nil                           
         generate (succ a) => cons (succ a) (generate a)
       }                                                
     }                                                  
------------------------------------------------------------------------------
inspect generate (succ (succ (succ zero)))                  
          =>                                                
          cons (succ (succ (succ zero)))                    
          % (cons (succ (succ zero)) (cons (succ zero) nil))
           : List Nat                                       
------------------------------------------------------------------------------
     (      a : Nat      !                            
let  !-------------------!                            
     ! factorial a : Nat )                            
                                                      
     factorial a => foldl mul (succ zero) (generate a)
------------------------------------------------------------------------------
inspect factorial (succ (succ zero)) => succ (succ zero) : Nat
------------------------------------------------------------------------------
inspect map factorial (generate (succ (succ (succ zero))))   
          =>                                                 
          cons (succ (succ (succ (succ (succ (succ zero))))))
          % (cons (succ (succ zero)) (cons (succ zero) nil)) 
           : List Nat                                        
------------------------------------------------------------------------------


На предыдущую попытку (аналог map factorial [1..5]) ЖЖ сказал "Post too large." ;)

Пока у меня не получается редактировать уже полученные определения. Единственный путь - это Esc и Undo. Если Esc показал что-то неправильное, тогда Undo.

Не очень удобно, но жить можно.
Subscribe
  • Post a new comment

    Error

    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

  • 27 comments