Guillaume Duboc gldubc

## fun_app.md

      
        
          
            
              
              1 file
            
          
          
            
              
              0 forks
            
          
            
              
                
                0 comments
              
            
          
            
              
              0 stars
            
          
        
        
          
              
          
          
            
                gldubc
                / fun_app.md
            
            
              Last active
              February 25, 2026 16:57
            
              
                Function Application in Gradual Set-Theoretic Types
              
          
        
      
        

      
      
    Function Application in Gradual Set-Theoretic Types

These notes document the design and correctness of function application in
Elixir's gradual set-theoretic type system, as implemented in descr.ex.

1. Setup and Notation

We work in a gradual type system where types combine static and dynamic components.