nicodelpiano / stlcnat-exhaustivity-checker Goto Github PK
View Code? Open in Web Editor NEWAn exhaustivity checker for a small STLC+Nats language written in Haskell
License: MIT License
An exhaustivity checker for a small STLC+Nats language written in Haskell
License: MIT License
Eventually, we'll want to put this on Hackage, so let's start by packaging it up as a Cabal project. Later we can add it as a dependency in purescript
.
Match
class and its instances and functionstest-framework
?)I think we can write it like this:
instance Match Binder where
missed _ NullBinder = []
missed NullBinder b = go b
where
go Zero = [Succ NullBinder]
go (Succ n) = Zero : map Succ (go n)
missed Zero Zero = []
missed (Succ n) (Succ m) = map Succ (missed n m)
missed b _ = [b]
That is, we have four groups of cases:
NullBinder
matches everythingNullBinder
, we take the complement of the pattern[]
(this bit looks like unification)This should hopefully make it easier to generalize to other types of pattern.
Could you QuickCheck this to make sure it returns the same results?
For simplicity, we can just require that a pattern with guards has a fallback guard using otherwise
.
A type class makes the structure very clear in my opinion:
class Match c where
missed :: c -> c -> [c]
instance Match Binder where
missed Zero Zero = []
missed _ NullBinder = []
missed NullBinder b =
let all_pat = [Zero, Succ NullBinder]
in concat $ map (\cp -> missed cp b) all_pat
missed (Succ n) (Succ m) =
let ucs = missed n m
in (zip_con Succ) ucs
where
zip_con :: (Binder -> Binder) -> Case -> Case
zip_con _ [] = []
zip_con b bs = (b hps):rest
where
(hps, rest) = (head bs, tail bs)
missed b _ = [b]
(instance copied from your code)
Here's the neat bit. If you define a type of length-indexed lists:
{-# LANGUAGE GADTs, DataKinds #-}
data Nat = Z | S Nat
data Vec n a where
Nil :: Vec Z a
Cons :: a -> Vec n a -> Vec (S n) a
vecToList :: Vec n a -> [a]
vecToList Nil = []
vecToList (Cons x xs) = x : vecToList xs
instance (Show a) => Show (Vec n a) where
show Nil = "Nil"
show (Cons x xs) = "(Cons " ++ show x ++ " " ++ show xs ++ ")"
then you can define an instance
instance (Match c) => Match (Vec n c)
Once this instance is implemented, we have proved that the number of arguments matched by the output is the same as the number matched by the input! This is a very important invariant.
A declarative, efficient, and flexible JavaScript library for building user interfaces.
๐ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. ๐๐๐
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google โค๏ธ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.