PHI 11 - Type Constructors

11-type-constructors/.11-type-constructors.tex

@@ -0,0 +1,13 @@
+\documentclass[12pt]{article}
+% packages don't actually matter to pandoc afaik
+
+\begin{document}
+\section*{11-type-constructors}
+\today % pandoc doesn't handle \today. ./latex2md uses `date`
+\subsection*{Introduction}
+This proposal extends the type language with the machinery needed for parameterized type definitions.
+\subsubsection*{Example: Parametized Pairs}
+\begin{verbatim}
+type Pair a = (a, a) in
+\end{verbatim}
+\end{document}

11-type-constructors/11-type-constructors.md

@@ -0,0 +1,12 @@
+# 11-type-constructors
+
+2022-08-24
+
+## Introduction
+
+This proposal extends the type language with the machinery needed for
+parameterized type definitions.
+
+### Example: Parametized Pairs
+
+    type Pair a = (a, a) in

11-type-constructors/README.md

@@ -0,0 +1,12 @@
+# 11-type-constructors
+
+2022-08-24
+
+## Introduction
+
+This proposal extends the type language with the machinery needed for
+parameterized type definitions.
+
+### Example: Parametized Pairs
+
+    type Pair a = (a, a) in

11-type-constructors/algo/Makefile

@@ -0,0 +1,3 @@
+.PHONY: test
+test:
+	cabal test --test-show-details=streaming

11-type-constructors/algo/algo.cabal

@@ -0,0 +1,55 @@
+cabal-version:      3.6
+name:               algo
+version:            0.1.0.0
+
+-- A short (one-line) description of the package.
+-- synopsis:
+
+-- A longer description of the package.
+-- description:
+
+-- A URL where users can report bugs.
+-- bug-reports:
+
+-- The license under which the package is released.
+-- license:
+author:             hejohns
+maintainer:         [email protected]
+
+-- A copyright notice.
+-- copyright:
+-- category:
+extra-source-files: CHANGELOG.md
+
+library
+    exposed-modules:  Algo
+    hs-source-dirs:   src
+    other-modules:    Common
+                      External
+                      Internal
+                      ECtx
+                      ICtx
+                      Normalize
+                      BiDirectional
+    build-depends:    base ^>=4.16.0.0
+                     ,hs-perl5
+                     ,shqq
+    default-language: GHC2021
+    ghc-options:      -Wall -Wno-unused-matches
+
+test-suite test-algo
+    type:             exitcode-stdio-1.0
+    main-is:          Tests.hs
+    hs-source-dirs:   test
+    other-modules:    Lexer
+                      Parser
+    build-depends:    base ^>=4.16.0.0
+                     ,HUnit
+                     ,algo
+                     ,array
+    default-language: GHC2021
+    -- man perlembed: `perl -MExtUtils::Embed -e ccopts -e ldopts`
+    -- and then pruned for stuff ghc doesn't understand
+    -- NOTE: yes, I know cabal complains about using ghc-options this way
+    -- but this is easier to manage for me, the human
+    ghc-options:      -Wall -L/usr/local/lib  -L/usr/lib/x86_64-linux-gnu/perl/5.34/CORE -lperl -ldl -lm -lpthread -lc -lcrypt -D_REENTRANT -D_GNU_SOURCE -DDEBIAN -I/usr/local/include -D_LARGEFILE_SOURCE -D_FILE_OFFSET_BITS=64 -I/usr/lib/x86_64-linux-gnu/perl/5.34/CORE

11-type-constructors/algo/cabal.project

@@ -0,0 +1,10 @@
+packages: ./*.cabal
+jobs: $ncpus
+optimization: 0
+profiling: True
+profiling-detail: all-functions
+
+source-repository-package
+  type: git
+  location: https://github.com/phlummox/hs-perl5.git
+  tag: 22d1aa69c4f101873c81ac9a2ff4a208a96cd1d4

11-type-constructors/algo/src/Algo.hs

@@ -0,0 +1,14 @@
+module Algo
+  ( module Algo -- does nothing right now
+  , module Common
+  , module Normalize -- to call algorithms
+  , module ECtx -- initial contexts
+  , module External -- so we can write types
+  , module BiDirectional
+  ) where
+
+import BiDirectional hiding ((⊳→))
+import Common
+import ECtx
+import External
+import Normalize

11-type-constructors/algo/src/BiDirectional.hs

@@ -0,0 +1,72 @@
+{-# LANGUAGE PostfixOperators #-}
+{-# LANGUAGE RecordWildCards #-}
+{-# LANGUAGE DuplicateRecordFields #-}
+{-# LANGUAGE OverloadedRecordDot #-}
+
+module BiDirectional where
+
+import Common
+import Data.Maybe
+import qualified ECtx
+import qualified External as E
+import qualified ICtx
+import qualified Internal as I
+import Normalize hiding ((⊳→))
+
+syn :: ECtx.Ctx -> E.Exp -> Maybe I.Term
+syn eΓ eδ = do
+  iΓ <- fixCtx eΓ
+  syn' iΓ eδ
+
+syn' :: ICtx.Ctx -> E.Exp -> Maybe I.Term
+syn' iΓ (E.EVar t) = ICtx.lookupE iΓ t
+syn' iΓ (E.Eλ x eτ eδ) = do
+  SER {term = iδ1, ..} <- syn_elab' iΓ eτ
+  iδ2 <- syn' (iΓ ICtx.⌢⌢⌢ (x, iδ1)) eδ
+  return $ iδ1 I.:⊕ iδ2
+syn' iΓ (E.EAp eδ1 eδ2) = do
+  iδ1 <- syn' iΓ eδ1
+  let MATR {..} = iΓ ⊢ (iδ1 ⊳→)
+  ana iΓ eδ2 iδIn &>> return iδOut
+syn' iΓ (E.ETypLet t eτ eδ) = do
+  SER {typ = iτ, term = iδ, ..} <- syn_elab' iΓ eτ
+  let innerΓ = (iΓ ICtx.⌢ (t, iτ))
+  iδ' <- syn' innerΓ eδ
+  return $ insensitiveβnormal (subst iδ t iδ')
+syn' iΓ (E.EExpLet x eτ eδDef eδBody) = do
+  SER {term = iδ, ..} <- syn_elab' iΓ eτ
+  ana iΓ eδDef iδ &>> syn' (iΓ ICtx.⌢⌢⌢ (x, iδ)) eδBody
+
+ana :: ICtx.Ctx -> E.Exp -> I.Term -> Bool
+ana iΓ eδ iδ' = fromMaybe False (syn' iΓ eδ >>= \iδ -> Just (iΓ ⊢ (iδ ~ iδ' $ I.Type)))
+
+data MATResult =
+  MATR
+    { iδIn :: I.Term
+    , iδOut :: I.Term
+    }
+  deriving (Show)
+
+-- TODO: type suggests this is to be generalized to ``consistent sub type (constructor)''
+-- but right now is only ``consistent sub type (at kind Type)''
+cst' :: ICtx.Ctx -> I.Term -> I.Term -> I.Typ -> Bool
+cst' _ (I.ETHole _) _ _ = True
+cst' _ _ (I.ETHole _) _ = True
+cst' _ (I.NETHole _ _) _ _ = True
+cst' _ _ (I.NETHole _ _) _ = True
+cst' iΓ (iδ1 I.:⊕ iδ2) (iδ1' I.:⊕ iδ2') iτ =
+  cst' iΓ iδ1 iδ1' iτ && cst' iΓ iδ2 iδ2' iτ
+cst' iΓ iδ1 iδ2 iτ = tequiv' iΓ iδ1 iδ2 iτ
+
+(~) :: I.Term -> I.Term -> I.Typ -> ICtx.Ctx -> Bool
+(~) = ((.) . (.) $ flip) . ((.) flip) . flip $ cst'
+
+mat' :: ICtx.Ctx -> I.Term -> MATResult
+mat' _ (I.ETHole u) = MATR (I.ETHole u) (I.ETHole u)
+mat' _ (iδ1 I.:⊕ iδ2) = MATR iδ1 iδ2
+mat' aΓ δ =
+  case wh_reduc aΓ δ of
+    Left _ -> error $ "Can't (⊳→) on this bogus value: " ++ (show aΓ) ++ " ⊢ " ++ (show δ)
+    Right δ' -> mat' aΓ δ'
+
+(⊳→) = flip mat'

11-type-constructors/algo/src/Common.hs

@@ -0,0 +1,95 @@
+-- NOTE: we alwys assume programs are α-renamed so no shadowing occurs
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE QuasiQuotes #-}
+
+module Common where
+
+import Control.Monad (MonadPlus, mzero)
+import Language.Perl
+import System.IO.Unsafe
+import System.ShQQ
+
+type TID = String
+
+type HID = Int
+
+class Eq a =>
+      Rewrite a
+  {-
+   - (==) must be ≡_α
+   -}
+  where
+  type RW a
+  (≡) :: a -> a -> Bool
+  (≡) = (==)
+  {-
+   - okay, not exactly an alpha-conversion,
+   - but replaces all instances of a variable with another
+   -}
+  αRename :: TID -> TID -> a -> a
+  subst :: RW a -> TID -> a -> a
+
+infix 4 ≡
+
+-- utilities:
+(&>>) :: MonadPlus m => Bool -> m a -> m a
+(&>>) True = id
+(&>>) False = \_ -> mzero
+
+infix 2 &>>
+
+-- when Γ is the first argument
+(⊢) :: a -> (a -> b) -> b
+aΓ ⊢ f = f aΓ
+
+-- when Γ is the last argument
+(|>) :: a -> (a -> b) -> b
+aΓ |> f = f aΓ
+
+infixl 2 |>
+
+fresh :: TID -> TID
+fresh t =
+  let p =
+        "my $tid = '" ++
+        t ++
+        "';" ++
+        "$tid =~ /(\\D+)(\\d+)?/;" ++
+        "if(defined $2){" ++
+        "$_ = $1 . ($2 + 1)" ++ "} else{" ++ "$_ = $1 . '1'" ++ "}"
+   in let pp = p ++ "; print"
+       in unsafePerformIO $ [sh| perl -e $pp |]
+
+{-
+  withPerl $
+  eval $
+-}
+fresh2 :: TID -> TID -> TID
+fresh2 t t' =
+  let p =
+        "my $tid1 = '" ++
+        t ++
+        "';" ++
+        "my $tid2 = '" ++
+        t' ++
+        "';" ++
+        "$tid1 =~ /(\\D+)(\\d+)?/;" ++
+        "my ($tid1_1, $tid1_2) = ($1, $2);" ++
+        "$tid2 =~ /(\\D+)(\\d+)?/;" ++
+        "my ($tid2_1, $tid2_2) = ($1, $2);" ++ "$_ = $tid1_1 . $tid2_1 . '1'"
+   in let pp = p ++ "; print"
+       in unsafePerformIO $ [sh| perl -e $pp |]
+
+{-
+  withPerl $
+  eval $
+-}
+freshfresh :: TID
+freshfresh =
+  let p = "$_ = 'mpk' . time()"
+   in let pp = p ++ "; print"
+       in unsafePerformIO $ [sh| perl -e $pp |]
+{-
+withPerl $ eval $
+-}

11-type-constructors/algo/src/ECtx.hs

@@ -0,0 +1,40 @@
+module ECtx where
+
+import Common
+import External
+
+type EAssump = (TID, Typ)
+
+type TAssump = (TID, Knd)
+
+data Ctx
+  = Nil
+  | Ctx :⌢ TAssump
+  | Ctx :⌢⌢⌢ EAssump
+  deriving (Show)
+
+lookupT :: Ctx -> TID -> Maybe Knd
+lookupT Nil _ = Nothing
+lookupT (aΓ :⌢ (t', κ)) t
+  | t' == t = Just κ
+  | otherwise = lookupT aΓ t
+lookupT (aΓ :⌢⌢⌢ _) t = lookupT aΓ t
+
+lookupE :: Ctx -> TID -> Maybe Typ
+lookupE Nil _ = Nothing
+lookupE (iΓ :⌢ _) t = lookupE iΓ t
+lookupE (iΓ :⌢⌢⌢ (t', τ)) t
+  | t' == t = Just τ
+  | otherwise = lookupE iΓ t
+
+(⌢) :: Ctx -> TAssump -> Ctx
+(⌢) aΓ tassump@(t, _κ) =
+  case lookupT aΓ t of
+    Just _ -> error "Do not shadow"
+    Nothing -> aΓ :⌢ tassump
+
+(⌢⌢⌢) :: Ctx -> EAssump -> Ctx
+(⌢⌢⌢) aΓ eassump@(x, _τ) =
+  case lookupE aΓ x of
+    Just _ -> error "Do not shadow"
+    Nothing -> aΓ :⌢⌢⌢ eassump