gelisam

{-# LANGUAGE NullaryTypeClasses, Rank2Types #-}
import Prelude hiding (log)
import Unsafe.Coerce
import System.IO.Unsafe


class NeedsInit

provideInit :: (NeedsInit => a) -> (() -> a)
provideInit = unsafeCoerce

gelisam

-- in reply to http://www.reddit.com/r/haskell/comments/1zf3ay/trying_to_design_a_gui_library/

{-# LANGUAGE ExistentialQuantification #-}

import Text.Printf


type Key = String

data Widget s = Widget

gelisam

-- In response to [1].
-- 
-- I am aiming for readability, not conciseness. Nevertheless, a note
-- explaining why the original javascript code is so much shorter:
-- Javascript skips all error checking unless you perform explicit checks.
-- Haskell enforces all error checking unless you explicitly ignore errors.
-- I have thus implemented many wrapping functions whose purpose is to use
-- incomplete pattern-matching to ignore errors.
-- 
-- I am using the aeson package for JSON and the download-curl package for

gelisam

{-# LANGUAGE GADTs, StandaloneDeriving, TypeFamilies, MultiParamTypeClasses #-}
module Main where

import Data.Word


type family Promote a b where
  Promote Word8  Word16 = Word16
  Promote Word16 Word8  = Word16
  Promote a a = a

gelisam

-- A small imperative language with a single anonymous mutable variable.
-- In response to http://www.reddit.com/r/haskell/comments/207mcn/binding_type_variables_using_the_bound_library/
{-# LANGUAGE DeriveFunctor #-}
module Main where

import Control.Monad.Trans.Class
import Control.Monad.Trans.State
import Bound

gelisam

// primitive types which cannot be signed
  //void ordinary_void;
  bool ordinary_bool;
  float ordinary_float;
  double ordinary_double;
  long double ordinary_long_double;
// types which can be signed
  // char
    char ordinary_signed_char;
    signed char explicit_signed_char;

gelisam

% in reply to http://www.reddit.com/r/haskell/comments/23cajh/how_can_i_avoid_this_function_to_typecheck/

% the datatype nat, with constructors z and s.
nat : type.
z : nat.
s : nat -> nat.

% a bunch of synonyms
zero  = z               : nat.
one   = s z             : nat.

gelisam

{-# LANGUAGE RankNTypes #-}

applyId :: (forall a. a -> a) -> b -> b
applyId f = f

passes :: [b] -> [b]
passes = map (applyId id)

-- works with ghc 7.6, fails with ghc 7.8
fails :: [b] -> [b]

gelisam

-- in reply to http://www.reddit.com/r/haskell/comments/26dshj/why_doesnt_haskell_allow_type_aliases_in_the/
module Main where

open import Data.Nat
open import Data.List renaming (monad to List-Monad)
open import Category.Monad
open import Relation.Binary.PropositionalEquality


-- Unlike Haskell, Agda supports arbitrary functions from type to type.

gelisam

import Control.Applicative
import Control.Monad
import Graphics.Rendering.OpenGL.GL  -- from package "OpenGL"
import Graphics.UI.GLFW as GLFW      -- from package "GLFW-b"

windowWidth, windowHeight :: Int
(windowWidth, windowHeight) = (640, 480)

initialDots :: [Vector2 GLfloat]
initialDots = [ Vector2 0.5 0.5