chrisdone

Type Inference: Various Designs

I'm exploring the right data types for writing a type inference with higher kinds and poly types.

Putting more things in the type system can force you to think about more things, but it also can make it harder and more verbose to write and read algorithms.

• This one implements a fairly good type inferer, with a free monad, but kinds are not enforced, and forall/schemes are not considered atll.
• This one pushes kinds and generic vars into the type system with a nested tuples approach
• This one borrows from Oleg's typed eval, but doesn't actually implement any hard things yet.

chrisdone

{-# LANGUAGE TypeOperators, LambdaCase, StandaloneDeriving, GADTs #-}

data Type env t where
  -- A constant type. Add kinds?
  -- Maybe, (), Int, Either, (->), etc.
  Constructor :: kind -> Type env kind
  -- A free variable.
  -- a
  FreeVariable :: kind -> Type env kind
  -- Type application.

chrisdone

-- Credit to: https://news.ycombinator.com/item?id=15186988

let iterate
    : (Natural → Natural) → Natural → Natural
    =   \f n ->
          fold (n + 1) f 1

let increment : Natural → Natural = \n -> n + 1

let ackermann

chrisdone

{-# LANGUAGE Strict #-}
{-# LANGUAGE Strict #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE RankNTypes, InstanceSigs, KindSignatures, GADTs, ConstraintKinds, ScopedTypeVariables #-}

-- http://neilsculthorpe.com/publications/constrained-monad-problem.pdf

import           Data.Function
import           Data.List.NonEmpty (NonEmpty(..))

chrisdone

{-# LANGUAGE RankNTypes, InstanceSigs, KindSignatures, GADTs, ConstraintKinds, ScopedTypeVariables #-}

-- http://neilsculthorpe.com/publications/constrained-monad-problem.pdf

import GHC.Exts

data NAF :: (* -> Constraint) -> (* -> *) -> * -> * where
  Pure :: a -> NAF c t a
  Ap :: c x => NAF c t (x -> a) -> t x -> NAF c t a

chrisdone

{-# LANGUAGE RankNTypes, InstanceSigs, KindSignatures, GADTs, ConstraintKinds #-}

-- Paper: http://neilsculthorpe.com/publications/constrained-monad-problem.pdf
-- Talk: https://vimeo.com/69261960

import GHC.Exts

data NF :: (* -> Constraint) -> (* -> *) -> * -> * where
  FMap :: c x => (x -> a) -> t x -> NF c t a

chrisdone

{-# LANGUAGE OverloadedStrings #-}

-- |

module RIO.ConcurrentLog where

import qualified Data.ByteString.Builder as SB
import           Data.List
import           Data.Time
import           RIO

chrisdone

applicative :: Q Exp -> [Q Exp] -> Q Exp
applicative cons [] = [| pure $(cons) |]
applicative cons (x:ys) = foldl (\inner y -> [| $(inner) <*> $(y) |]) [|$(cons) <$> $(x)|] ys

chrisdone

-- | Conduit piping with error handling.

module Data.Conduit.Error where

import Data.Conduit.Internal

infixr 2 .|?
(.|?) :: Monad m => ConduitT a b m (Either e ()) -> ConduitT b c m (Either e r) -> ConduitT a c m (Either e r)
ConduitT left0 .|? ConduitT right0 =
  ConduitT $ \rest ->

chrisdone

{-# LANGUAGE LambdaCase #-}

-- | Sources that flush when their monadic action takes longer than n
-- microseconds.

module Data.Conduit.Flush where

import Data.Conduit
import Data.Conduit.Internal as Pipe (ConduitT(..), Pipe(..))
import UnliftIO