maiermic

module reverse_hvect

import Data.HVect

reverse : HVect ts -> HVect (reverse ts)
reverse [] = []
reverse (x::xs) = (reverse xs) ++ [x]

maiermic

module reverse_vect

import Data.Vect

myReverse : Vect n a -> Vect n a
myReverse [] = []
myReverse (x::xs) = (myReverse xs) ++ [x]

maiermic

module reverse_hvect

import Data.Vect
import Data.HVect

myReverse : Vect n a -> Vect n a
myReverse [] = []
myReverse {n = S k} (x::xs) = rewrite plusCommutative 1 k in (myReverse xs) ++ [x]

reverse : HVect ts -> HVect (myReverse ts)

maiermic

class MyTuple<out Element, out First, out Rest = []>
		(first, rest)
		extends Object()
		satisfies List<Element>
		given First satisfies Element
		given Rest satisfies List<Element>
{
	"The first element of this tuple. (The head of the 
	    linked list.)"
	shared actual 

maiermic

When checking argument f to function Prelude.Basics.flip:
        Type mismatch between
                Type -> Type -> Type (Type of Pair)
        and
                a -> b1 -> b -> c -> Type (Expected type)

        Specifically:
                Type mismatch between
                        Type
                and

maiermic

unzip_hvect.idr:7:1-6:When checking left hand side of unzip_hvect.unzip:
When checking an application of unzip_hvect.unzip:
        Type mismatch between
                HVect [] (Type of [])
        and
                HVect (zipWith (\t1 => \t2 => (t1, t2)) ts1 ts2) (Expected type)

        Specifically:
                Type mismatch between
                        []

maiermic

generated with DocToc then modified with Sublime Text 3 (add links):

• select all # of the TOC using multiple cursors (CTRL + D)
• move cursors two characters ]( left
• select content between brackets (CTRL + M)
• use Case Conversion plugin command dash-case
• copy selection
• undo dash-case
• move cursors back after the # character
• paste clipboard

maiermic

Overview and comparison of generic type syntax proposals

This issue lists and compares several syntax proposals that have been proposed and initially discussed in issue #55. It should help to come to a decision which syntax proposal should be used.

Note: The following aspects have not been discussed yet and are not part of this overview/comparison:

• variance (covariant, contravariant and invariant)
• type restrictions

maiermic

Variance

The term variance describes how subtyping between higher kinded types is related to subtyping relations of their type arguments.

Higher Kinded Types

A higher kinded type composes type arguments to a new type. I use square bracket notation to define a higher kinded type:

C[T] // The higher kinded type `C` composes type argument `T` to a new type `C[T]`.

The same works with multiple type arguments:

maiermic

Performing configuration checks

    - 32-bit                   : no
    - 64-bit                   : yes
    - x86                      : yes
    - has_icu builds           : no
warning: Graph library does not contain MPI-based parallel components.
note: to enable them, add "using mpi ;" to your user-config.jam
    - iconv (libc)             : yes
    - icu                      : no