Functional Programming

Haskell » History » Revision 5

Revision 4 (Grigoriy Volkov, 12/14/2018 04:41 PM) → Revision 5/90 (Grigoriy Volkov, 01/22/2019 04:19 PM)

h1. Haskell 

 "Haskell Cheatsheet":http://bxt.github.io/Ludus/haskell-cheatsheet/ 

 h2. snippets 

 * [[HaskellMaybeChecks]] 
 * [[HaskellTypeLevelMachine]] 

 h2. libs 

 * "concat":https://github.com/conal/concat ("z3cat":https://github.com/jwiegley/z3cat/blob/master/test/Main.hs || "smt example":https://github.com/conal/concat/blob/master/examples/src/ConCat/SMT.hs) — *"Compiling to categories":http://conal.net/papers/compiling-to-categories/* — compiler plugin for translating normal Haskell functions (on standard types) to SMT, etc. 
 * "SBV: SMT Based Verification":https://leventerkok.github.io/sbv/ — translates Haskell functions on custom symbolic types 
 * "refined":http://nikita-volkov.github.io/refined/ — refinement types <pre>type ProperFraction = Refined (And (Not (LessThan 0)) (Not (GreaterThan 1))) Double</pre> 
 * "hedgehog":https://github.com/hedgehogqa/haskell-hedgehog — random test gen (QuickCheck) 
 * "GHC.Stack":https://hackage.haskell.org/package/base-4.10.0.0/docs/GHC-Stack.html — can get code position for DSL 
 * "Data.Sequence":http://hackage.haskell.org/package/containers-0.6.0.1/docs/Data-Sequence.html — list with fast append on both sides 

 h2. exts 

 * "RebindableSyntax":https://ocharles.org.uk/guest-posts/2014-12-06-rebindable-syntax.html — overloading built-in operators / do notation 
 * "NullaryTypeClasses":https://ocharles.org.uk/posts/2014-12-10-nullary-type-classes.html — global implementation of one thing 

 h2. snippets 

 h3. Using Maybe Monad for checks 

 <pre> 
 * "DataKinds":http://ponies.io/posts/2014-07-30-typelits.html , TypeFamilies (+ GHC.TypeLits) — type-level annotations {-# LANGUAGE LambdaCase, RecordWildCards #-} 

 import Data.Maybe (isJust, mapMaybe) 
 ** "Basic Type Level Programming in Haskell":https://www.parsonsmatt.org/2017/04/26/basic_type_level_programming_in_haskell.html import Data.List (nub) 

 data Group = X25519 | Secp384 
            deriving (Eq) 

 data KeyShareData = KeyShareClientHello [Group] 
                   | KeyShareHelloRetryRequest Group 

 data Ext = SupportedGroups [Group] 
          | KeyShares KeyShareData 

 check :: [Ext] -> [Ext] -> Bool 
 ** "Parsing type-level strings in Haskell":https://kcsongor.github.io/symbol-parsing-haskell/ check eCH eHRR = isJust $ do 
   sgCH <- exactlyOne $ mapMaybe (\case SupportedGroups gs -> Just gs; _ -> Nothing) eCH 
   continueIf $ nub sgCH == sgCH -- no duplicates allowed 
   ksCH <- (\case KeyShareClientHello gs -> Just gs; _ -> Nothing) =<< 
     exactlyOne (mapMaybe (\case KeyShares ks -> Just ks; _ -> Nothing) eCH) 
   ksHRR <- (\case KeyShareHelloRetryRequest g -> Just g; _ -> Nothing) =<< 
     exactlyOne (mapMaybe (\case KeyShares ks -> Just ks; _ -> Nothing) eHRR) 
   continueIf $ nub ksCH == ksCH -- no duplicates allowed 
   continueIf $ ksHRR `elem` sgCH -- group must be supported 
   continueIf $ ksHRR `notElem` ksCH -- key share must not have been already sent 

 exactlyOne :: [a] -> Maybe a 
 ** "Servant, Type Families, and Type-level Everything":https://arow.info/blog/posts/2015-07-10-servant-intro.html exactlyOne [x] = Just x 
 ** "Haskell Type Names as Strings":http://www.mchaver.com/posts/2017-12-12-type-name-to-string.html exactlyOne _ = Nothing 

 continueIf :: Bool -> Maybe () 
 continueIf True = Just () 
 continueIf False = Nothing 
 </pre>