Skip to content

Instantly share code, notes, and snippets.

View aradarbel10's full-sized avatar

Arad Arbel aradarbel10

9 followers · 12 following
View GitHub Profile
@aradarbel10
aradarbel10 / Main.hs
Last active June 14, 2023 20:52
Type directed program synthesis for STLC
{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
{-# HLINT ignore "Use list comprehension" #-}
import Data.IORef ( IORef, newIORef, readIORef, writeIORef )
import GHC.IO ( unsafePerformIO )
import Control.Applicative ( Alternative(..) )
import Control.Monad ( when )
import Debug.Trace
@aradarbel10
aradarbel10 / natcomp.lagda.md
Last active June 14, 2023 20:28
A tiny formally-verified compiler from arithmetic expressions to a stack machine 
module natcomp where

open import Data.Nat using (ℕ; _+_)
open import Data.List using (List; []; _∷_; _++_)
open import Data.List.Properties using (++-assoc)
open import Data.Maybe using (Maybe; just; nothing; _>>=_)

open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong)
open Relation.Binary.PropositionalEquality.≡-Reasoning
@aradarbel10
aradarbel10 / main.ml
Last active July 3, 2023 15:12
minimal STLC type inference with mutable metavars
(* language definition *)
type nom = string
type bop = Add | Sub | Mul
type typ =
| Int | Arrow of typ * typ | Meta of meta
and meta = meta_state ref
and meta_state =
| Solved of typ
| Unsolved of nom (* keep name for pretty printing *)
@aradarbel10
aradarbel10 / Main.hs
Created December 6, 2022 15:40
A minimalistic example of bidirectional type checking for system F
{-# LANGUAGE StrictData, DerivingVia, OverloadedRecordDot #-}
{-
(compiled with GHC 9.4.2)
-}
{-
HEADS UP
this is an example implementation of a non-trivial type system using bidirectional type checking.
it is...
@aradarbel10
aradarbel10 / contexts.lagda.md
Last active September 19, 2022 02:41
Category of contexts and context-renamings 
{-# OPTIONS --without-K #-}

open import foundation.functions using (_∘_)
open import foundation.identity-types using (refl; ap) renaming (Id to _≡_)

Contexts

We think of contexts as snoc lists of types




  


  




    


          
    

      

        
        

          

              @aradarbel10
          

          

            
                aradarbel10
                / parser_simple.mly
            
            

              Last active
              September 6, 2022 22:00
            

              
                Menhir (LR) grammar for pi types with syntactic sugar `(x y z : a) -> b` and `a -> b`
              
          

        

      

        

  

    
    


        



  


  

        

          
          %{
        

        

          
          (** the [Surface] module contains our AST. *)
        

        

          
          open Surface
        

        

          
          

        

        

          
          (** exception raised when a [nonempty_list] returns an empty list. *)
        

        

          
          exception EmptyUnfolding
        

        

          
          

        

        

          
          (** desugars `(x y z : a) -> b` into `(x : a) -> (y : a) -> (z : a) -> b`. *)
        

        

          
          let rec unfoldPi (xs : string list) (dom : expr) (cod : expr) : expr =
        

        

          
            match xs with
        

  





    


  




    


          
    

      

        
        

          

              @aradarbel10
          

          

            
                aradarbel10
                / groupoid.agda
            
            

              Created
              July 13, 2022 09:11
            

              
                Direct proof for groupoidal structure of homotopic identity types via path induction in Agda
              
          

        

      

        

  

    
    


        



  


  

        

          
          {-# OPTIONS --without-K #-}
        

        

          
          

        

        

          
          import Relation.Binary.PropositionalEquality as Eq
        

        

          
          open Eq using (_≡_; refl)
        

        

          
          

        

        

          
          pattern erefl x = refl {x = x}
        

        

          
          

        

        

          
          

        

        

          
          --- path induction ---
        

        

          
          J : ∀ {A : Set} →