sebfisch

tyFun : Set -> Set -> Set;
tyFun A T = A -> T;

using (G:Vect Set n) {

  data Expr : Vect Set n -> Set -> Set where
    Var : (i:Fin n) -> Expr G (vlookup i G)
  | Val : T -> Expr G T
  | Lam : Expr (A::G) T -> Expr G (tyFun A T) -- using `A -> T` directly fails
  | App : Expr G (A -> T) -> Expr G A -> Expr G T

sebfisch

{- 

example from

    http://blog.downstairspeople.org/2010/06/14/a-brutal-introduction-to-arrows/

rewritten using Applicative instance from

    http://cdsmith.wordpress.com/2011/07/30/arrow-category-applicative-part-i/

sebfisch

{-# LANGUAGE TypeFamilies, TypeOperators, FlexibleContexts #-}

module GenericFoldableTraversable where

import Data.Monoid         ( Monoid, mappend, mempty )
import Data.Foldable       ( Foldable, foldMap )

import Control.Applicative ( Applicative, pure, (<*>) )
import Data.Traversable    ( Traversable, traverse )

sebfisch

This literate Haskell program implements a type safe interpreter for a
simple functional language. Such an interpreter is the "hello world"
example for dependently typed languages and this program mimics it in
Haskell. Generalized algebraic data types and type families are
sufficient.

> {-# LANGUAGE GADTs #-}
> {-# LANGUAGE TypeFamilies #-}
> {-# LANGUAGE TypeOperators #-}
> {-# LANGUAGE MultiParamTypeClasses #-}

sebfisch

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}

import Data.Function ( fix )
import Data.MemoTrie        -- from package MemoTrie
import Data.MemoCombinators -- from package data-memocombinators

main :: IO ()
main =
  -- without caching

sebfisch

diff --git a/bluetile.cabal b/bluetile.cabal
index 5ccc294..fd358e6 100644
--- a/bluetile.cabal
+++ b/bluetile.cabal
@@ -1,5 +1,5 @@
 Name:                bluetile
-Version:             0.5.3
+Version:             0.5.3.1
 homepage:            http://www.bluetile.org/
 synopsis:            full-featured tiling for the GNOME desktop environment

sebfisch

#include <iostream>
#include <string>
#include <re2/re2.h>

using namespace std;
using namespace re2;

int main(int argc, char* args[]) {
  // not syncing C++ and C I/O is faster with simple matchings
  ios_base::sync_with_stdio(false);

sebfisch

-- This snippet simulates naive dictionary passing for Curry type
-- classes using the explicit-sharing package for functional logic
-- programming in Haskell.
--
-- It defines a dictionary for the class
--
--   class Arb a where arb :: a
--
-- and a corresponding instance for the type Bool
--

sebfisch

-- Efficient solver for the n-queens problem in Curry.
--
-- A placement is represented as permutation of [1..n], each list
-- element represents the placement of a queen in the column
-- corresponding to its index.

-- The implementation uses a finite domain constraint solver which is
-- available in the Curry system PAKCS.
--
import CLPFD

sebfisch

-- Simple solver for the n-queens problem in Curry.
--
-- A placement is represented as permutation of [1..n], each list
-- element represents the placement of a queen in the column
-- corresponding to its index.

import Integer ( abs )

-- Solutions are computed using a lazy generate-and-test approach:
-- candidate solutions are created lazily and admissible solutions