Skip to content

Instantly share code, notes, and snippets.

View gelisam's full-sized avatar

Samuel Gélineau gelisam

267 followers · 26 following
View GitHub Profile
@gelisam
gelisam / PolymorphicStrictness.hs
Last active August 29, 2015 14:04
code polymorphic in strictness (proof of concept)
-- in response to http://www.reddit.com/r/haskell/comments/2chb2h/fantasy_world_haskell/cjfobm5
--
-- Here is a demonstration that it is possible to write code which is "polymorphic in strictness",
-- that is, which can be executed strictly or lazily depending on the type at which it is instantiated.
--
-- Note that such a polymorphic function has to ask for a custom implementation of fmap and any other
-- standard function it is using, because those functions are not themselves polymorphic in strictness.
import Control.DeepSeq
import Debug.Trace
@gelisam
gelisam / PolymorphicStrictness2.hs
Created August 5, 2014 04:41
datatypes polymorphic in strictness
-- a better version of https://gist.github.com/gelisam/58495f7b996f77e09d80
-- based on http://www.reddit.com/r/haskell/comments/2chb2h/fantasy_world_haskell/cjgepwj
--
-- I implement the same example three times: once with a lazy datatype,
-- once with a strict datatype, and once with a strict-polymorphic datatype.
{-# LANGUAGE BangPatterns, KindSignatures, TypeOperators #-}
import Debug.Trace
import Text.Printf
@gelisam
gelisam / Main.hs
Last active August 29, 2015 14:09
Variations on self-memoizing html
-- in reply to http://www.reddit.com/r/haskell/comments/2m2d03/selfmemoizing_html_rendering_via_mutually/
-- this is a version were the trie is stored with the render function instead of inside the tree.
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module Main where
import Debug.Trace
import Data.Monoid
@gelisam
gelisam / Main.idr
Last active August 29, 2015 14:12
How Type-in-Type in Idris can lead to a contradiction.
-- Idris version of https://gist.github.com/gelisam/5152919,
-- which is now correctly caught by Agda, but not by Idris as of 0.9.15.1-git:b0257ec
module Main
-- caught by the totality checker
--bottom : Void
--bottom = bottom
subst : {p : Type -> Type, x : Type, y : Type} -> x = y -> p y -> p x
@gelisam
gelisam / Main.hs
Created May 23, 2015 13:43
Strictness-polymorphic ListT
-- In response to a similar implementation in an imaginary strict Haskell-like language
-- (http://www.reddit.com/r/haskell/comments/36ysso/if_haskell_were_strict_what_would_the_laziness_be/)
module Main where
import Debug.Trace
import Text.Printf
-- Note that this cannot be a newtype or the !(m a) below will collapse to !a
@gelisam
gelisam / Main.agda
Created March 13, 2013 14:58
How Agda's --type-in-type can lead to a contradiction.
{-# OPTIONS --type-in-type #-}
module Main where
open import Data.Empty
data _≡_ (A : Set) : Set → Set where
refl : A ≡ A
subst : {P : Set → Set} → {x y : Set} → x ≡ y → P y → P x
@gelisam
gelisam / memoizing_fib.hs
Last active December 21, 2015 05:38
Polymorphism and memoization interact in strange ways.
import Debug.Trace
noisy0 :: () -> Int
noisy0 () = trace "eval" 0
main = do print (let x = ( noisy0 ()
, fst x)
in x) -- evals noisyMempty once
print (( noisy0 ()
@gelisam
gelisam / README.md
Last active December 22, 2015 09:19
To make the README very short and clear, we could delegate the details to a second, longer document.

Hawk

Transform text from the command-line using Haskell expressions. Similar to awk, but using Haskell as the text-processing language.

Examples

The Haskell expression (!! 1) takes the second element from a list. Using Hawk to --map this expression over all input lines, we can extract the second column of the output of ps aux.




  


  




    


          
    

      

        
        

          

              @gelisam
          

          

            
                gelisam
                / prelude.hs
            
            

              Last active
              December 22, 2015 10:29
            

              
                The ~/.hawk/prelude.hs you would need in order to run the tree command in the Hawk README.
              
          

        

      

        

  

    
    


        



  


  

        

          
          {-# LANGUAGE FlexibleInstances, OverloadedStrings #-}
        

        

          
          import Prelude
        

        

          
          import qualified Data.ByteString.Lazy.Char8 as B
        

        

          
          import qualified Data.List as L
        

        

          
          import Data.Monoid
        

        

          
          import Data.Tree hiding (Forest)
        

        

          
          import System.Console.Hawk.Representable
        

        

          
          

        

        

          
          

        

        

          
          newtype Forest a = Forest {unForest :: [Tree a]}
        

  





    


  




    


          
    

      

        
        

          

              @gelisam
          

          

            
                gelisam
                / Quine.hs
            
            

              Last active
              January 30, 2016 04:29
            

              
                A type-level Haskell quine
              
          

        

      

        

  

    
    


        



  


  

        

          
          {-# LANGUAGE DataKinds, TypeFamilies, TypeOperators, UndecidableInstances #-}
        

        

          
          module Quine where
        

        

          
          import GHC.TypeLits
        

        

          
          

        

        

          
          

        

        

          
          -- mod x y | x < y     = x
        

        

          
          --         | otherwise = mod (x - y) y
        

        

          
          

        

        

          
          type Mod x y = Mod'Guard x (CmpNat x y) y