chrisdone

{-# LANGUAGE DataKinds #-}

-- | My database API.

module DBAPI where

import Data.Defaults

data ConnSpec p = ConnSpec
  { username :: !(Required p String)

chrisdone

Proposal: Foreign Function Interface for Processes

Background

Thread with some poorly put together thoughts.

Limitations of Process Arguments

• Finite: All inputs to a program are finite. In every mainstream OS, arguments are a string of limited size. They are not

chrisdone

FROM debian:9-slim
MAINTAINER Chris Done

################################################################################
# Haskell system dependencies (basically never changes)

RUN apt-get update && \
    apt-get install -yq --no-install-suggests --no-install-recommends --force-yes -y -qq \
            netbase git ca-certificates xz-utils build-essential curl unzip libgmp-dev

chrisdone

instance Num a => Num (Q (TExp (SomeNamedWith IsNonzero a))) where
  fromInteger 0 = error "It's zero, fool!"
  fromInteger n = [|| someNamedWith IsNonzero (fromInteger n) ||]

fine :: Double
fine =
  case $$(1) :: SomeNamedWith IsNonzero Double of
    (SomeNamedWith p divisor) ->
      divide p 123 divisor
      

chrisdone

Statically checked overloaded strings

This gist demonstrates a trick I came up with which is defining IsString for Q (TExp a), where a is lift-able. This allows you to write $$("...") and have the string parsed at compile-time.

On GHC 9, you are able to write $$"..." instead.

This offers a light-weight way to enforce compile-time constraints. It's basically OverloadedStrings with static checks. The inferred return type

chrisdone

(CCall (CCallSpec (StaticTarget NoSourceText "integer_gmp_powm_word" (Just integer-gmp) True) CCallConv PlayRisky),(# State# RealWorld, Word# #))
(CCall (CCallSpec (StaticTarget NoSourceText "integer_gmp_powm" (Just integer-gmp) True) CCallConv PlayRisky),(# State# RealWorld, Int# #))
(CCall (CCallSpec (StaticTarget NoSourceText "integer_gmp_powm1" (Just integer-gmp) True) CCallConv PlayRisky),(# State# RealWorld, Word# #))
(CCall (CCallSpec (StaticTarget NoSourceText "integer_gmp_powm_sec" (Just integer-gmp) True) CCallConv PlayRisky),(# State# RealWorld, Int# #))
(CCall (CCallSpec (StaticTarget NoSourceText "integer_gmp_invert_word" (Just integer-gmp) True) CCallConv PlayRisky),(# State# RealWorld, Word# #))
(CCall (CCallSpec (StaticTarget NoSourceText "integer_gmp_invert" (Just integer-gmp) True) CCallConv PlayRisky),(# State# RealWorld, Int# #))
(CCall (CCallSpec (StaticTarget NoSourceText "__int_encodeDouble" (Just integer-gmp) True) CCallConv PlayRisky),(# State# RealWorld, Double# #))
(CCall (CCallSpec

chrisdone

(CCall (CCallSpec (StaticTarget NoSourceText "integer_gmp_powm_word" (Just integer-gmp) True) CCallConv PlayRisky),(# State# RealWorld, Word# #))
(CCall (CCallSpec (StaticTarget NoSourceText "integer_gmp_powm" (Just integer-gmp) True) CCallConv PlayRisky),(# State# RealWorld, Int# #))
(CCall (CCallSpec (StaticTarget NoSourceText "integer_gmp_powm1" (Just integer-gmp) True) CCallConv PlayRisky),(# State# RealWorld, Word# #))
(CCall (CCallSpec (StaticTarget NoSourceText "integer_gmp_powm_sec" (Just integer-gmp) True) CCallConv PlayRisky),(# State# RealWorld, Int# #))
(CCall (CCallSpec (StaticTarget NoSourceText "integer_gmp_invert_word" (Just integer-gmp) True) CCallConv PlayRisky),(# State# RealWorld, Word# #))
(CCall (CCallSpec (StaticTarget NoSourceText "integer_gmp_invert" (Just integer-gmp) True) CCallConv PlayRisky),(# State# RealWorld, Int# #))
(CCall (CCallSpec (StaticTarget NoSourceText "__int_encodeDouble" (Just integer-gmp) True) CCallConv PlayRisky),(# State# RealWorld, Double# #))
(CCall (CCallSpec

chrisdone

[2 of 2] Compiling Main             ( hask-tok3.hs, hask-tok3.o )

==================== Tidy Core ====================
Result size of Tidy Core
  = {terms: 2,614, types: 3,717, coercions: 1,413, joins: 31/63}

-- RHS size: {terms: 16, types: 9, coercions: 0, joins: 0/0}
Main.$WPoint [InlPrag=INLINE[2]] :: Int -> Int -> Int -> Point
[GblId[DataConWrapper],
 Arity=3,

chrisdone

-- | Our main engine for naming a value, then we can prove properties about a named value.

{-# LANGUAGE ExistentialQuantification #-} -- Used for SomeNamed.
{-# LANGUAGE PatternSynonyms #-} -- Used for the Name pattern.
{-# LANGUAGE ViewPatterns #-} -- Used for the Name pattern.
{-# LANGUAGE RankNTypes #-} -- Used for withName.

module Named ( Named, pattern Name, forgetName, withName, someNamed, SomeNamed(..) ) where

-- | Give a generated type-level name to any value.

chrisdone

Total (non-error-throwing) lambda-calculus evaluators.