sydneytypes / platypus Goto Github PK

View Code? Open in Web Editor NEW

This project forked from type-theory/type-theory-study-group

7.0 82.0 3.0 3.48 MB

Lunchtime type theory study group in Sydney

Home Page: https://www.meetup.com/Sydney-Type-Theory

TeX 75.62% Haskell 14.02% Idris 10.36%

type-theory functional-programming user-group sydney

platypus's Introduction

PLATYPUS

Type Theory Study Group

PLATYPUS^* is a study group meeting weekly in Sydney, Australia for people interested in learning more about type theory and its connections to programming languages.

Twitter @SydneyTypes
Meetup Sydney Type Theory

All are welcome!

Inspired by the online Type Theory Study Group 2015.

* Programming Languages and Types (yet perfectly understandable) in Sydney — thanks to Danny Gratzer for the name suggestion.

When and where

We meet on Monday lunchtimes from 12:30 to 2:00 pm.

Venue is the Commonwealth Bank of Australia, 255 Pitt Street Sydney.

Please RSVP via the Meetup page for catering purposes (and let us know if you have any particular dietary requirements).

Content

During 2015 and 2016 we read Bob Harper's Practical Foundations of Programming Languages, 2nd Edition.

In 2017 we're reading Simon Thompson's Type Theory and Functional Programming.

Agenda

For details on what we've covered and what we'll be reading next see the Meetup group

Resources

The online Type Theory Study Group

Type Theory Study Group on Google Groups
##typetheory on Freenode.net IRC
@type_theory on Twitter

Other resources

learn-tt is a great collection of resources for learning type theory.

Proposed Future Topics

The Untyped Lambda Calculus / Operational Semantics
The Simply Typed Lambda Calculus / Progress and Preservation
Propositions as Types / Proofs as Programs
System F / Parametricity
Martin-Löf's Extensional Type Theory / Constructive Mathematics and Computer Programming
Identity Types / Proofs of Equality in Martin-Löf's Intensional Type Theory
Topological Spaces as Types / Points as Programs
Intensional Proofs of Equality as Paths between Spaces
Proofs of Equality of Equalities as Synthetic Homotopies
Homotopy Type Theory / Higher Inductive Types / Univalence
Canonicity for Homotopy Type Theory / Current Issues
Special Cases of Homotopy Type Theory with Canonicity / Cubical Type Theories
Martin-Löf's (Equational) Logical Framework and the Monomorphic Theory of Sets
The Edinburgh Logical Framework / "Mechanizing Metatheory in a Logical Framework"
Categorical Semantics of Type Theories / Connection to Category Theory Study Group

platypus's People

Contributors

Stargazers

Watchers

Forkers

gitter-badger rowandavies rithvikshelke

platypus's Issues

Sequent Calculus Proof of Transitivity of Implication

Proving: (A → B) ∧ (B → C) ⊢ A → C

Me and Quoc worked on the above via the rules and guidance given on this page: http://sakharov.net/sequent.html We got:

------      ------
A |- A      B |- B
-------------------  -> left            ------
A -> B, A |- B                           C |- C
--------------------------------------------------  -> left
A, A -> B, B -> C    |-                      C
--------------------------------------------------  -> right
A -> B, B -> C       |-                      A -> C
---------------------------------------------------  &  left
(A -> B) & (B -> C), B -> C          |-      A -> C
---------------------------------------------------  &  left
(A -> B) & (B -> C), (A -> B) & (B -> C)  |- A -> C
---------------------------------------------------  C  left
(A -> B) & (B -> C)             |-           A -> C

However using: http://logitext.mit.edu/Intuitionistic/proving/.28A+.2D.3E+B.29+.2F.5C+.28B+.2D.3E+C.29+.7C.2D+.28A+.2D.3E+C.29 it shows us something like:

-----
C ⊢ C
----------- (W l)
B, C, A ⊢ C
--------------- (→ l)
B, B → C, A ⊢ C
--------------- (→ l)
A → B, B → C, A ⊢ C
------------------- (→ r)
A → B, B → C ⊢ A → C
------------------------- (∧ l)
(A → B) ∧ (B → C) ⊢ A → C

Which one is correct? Are they equivalent?

Also how can left implication be used in the second example when there isn't 2 subformulas on the top of the line?

@plintx

Functors for the "Generic Extensions to Type Operators"

I sometimes find it easier to understand if I relate the PFPL to equivalent constructs in Haskell.

Regarding today's meeting for page 123. We have a 5 polynomial type operators. Here are some equivalences I've found:

For 14.3.a:

map{t.t}(x.e')(e) -> [e/x]e'

> import Data.Functor.Identity
> instance (Show a) => Show (Identity a) where
> |     show (Identity a) = "Identity " ++ show a
> |
> fmap (\x -> x + 1) (Identity 3)
Identity 4
> :info Identity
newtype Identity a = Identity {runIdentity :: a}
        -- Defined in ‘Data.Functor.Identity’
instance Show a => Show (Identity a)
  -- Defined at <interactive>:24:10
instance Monad Identity -- Defined in ‘Data.Functor.Identity’
instance Functor Identity -- Defined in ‘Data.Functor.Identity’

For 14.3b:

map{t.unit}(x.e')(e) -> e

> import Data.Proxy
> fmap (\x -> x) Proxy
Proxy
it :: Proxy b
> :info Proxy
type role Proxy phantom
data Proxy (t :: k) = Proxy
        -- Defined in ‘Data.Proxy’
instance Bounded (Proxy s) -- Defined in ‘Data.Proxy’
instance Enum (Proxy s) -- Defined in ‘Data.Proxy’
instance Eq (Proxy s) -- Defined in ‘Data.Proxy’
instance Monad Proxy -- Defined in ‘Data.Proxy’
instance Functor Proxy -- Defined in ‘Data.Proxy’
instance Ord (Proxy s) -- Defined in ‘Data.Proxy’
instance Read (Proxy s) -- Defined in ‘Data.Proxy’
instance Show (Proxy s) -- Defined in ‘Data.Proxy’

There used to be a Data.Unit in category-extras package, but it was removed.

For 14.3c:

map{t.tau1 * tau2}(x.e')(e) -> <map{t.tau1}(x.e')(e.l),map{t.tau2}(x.e')(e.r)>

Unknown. Originally I thought it was a tuple. But it isn't. Also this is close data Pair a = Pair a a but it doesn't exactly match {t.tau1 * tau2}, it would be more like {t.t * t}.

For 14.3d:

map{t.void}(x.e')(e) -> abort(e)

Could be Data.Void, but it's not an instance of the Functor type class. Also I couldn't make it an instance of Functor because the kind is * and Functor needs a kind of * -> *.

> import Data.Void
> instance Functor Void where
> |     fmap _ v = absurd v
> |
    The first argument of ‘Functor’ should have kind ‘* -> *’,
      but ‘Void’ has kind ‘*’
    In the instance declaration for ‘Functor Void’

The closest thing to the same behaviour is...

> fmap (\x -> x) undefined
*** Exception: Prelude.undefined

For 14.3e:

map{t.tau1 + tau2}(x.e')(e) -> case e { l.x1 -> l.map{t.tau1}(x.e')(x1) | r.x2 -> r.map{t.tau2}(x.e')(x2) }

Not sure, could it be the Either functor?

How do denotational, axiomatic and operational semantics relate to statics and dynamics in PFPL?

Question in the title ^!

Continuing on the discussion on the applicability of HoTT

https://homotopytypetheory.org/category/applications/