haskell,types,binding,dependent-type , How can I express the type of 'takeWhile for vectors'?

## Question:

Haskell beginner here. I've defined the following types:

``````data Nat = Z | S Nat
data Vector a n where
Nil :: Vector a Z
(:-) :: a -> Vector a n -> Vector a (S n)
infixl 5 :-
``````

I'm trying to write the function, takeWhileVector which behaves the same as takeWhile does on lists, but on Vectors.

My implementation is as follows:

``````takeWhileVector :: (a -> Bool) -> Vector a n -> Vector a m
takeWhileVector f Nil = Nil
takeWhileVector f (x :- xs) = if (f x) then (x :- takeWhileVector f xs) else Nil
``````

This doesn't compile and produces the following error:

``````Could not deduce (m ~ 'S n0)
from the context (n ~ 'S n1)
bound by a pattern with constructor
:- :: forall a (n :: Nat). a -> Vector a n -> Vector a ('S n),
in an equation for ‘takeWhileVector’
at takeWhileVector.hs:69:20-26
‘m’ is a rigid type variable bound by
the type signature for
takeWhileVector :: (a -> Bool) -> Vector a n -> Vector a m
at takeWhileVector.hs:67:20
Expected type: Vector a m
Actual type: Vector a ('S n0)
Relevant bindings include
takeWhileVector :: (a -> Bool) -> Vector a n -> Vector a m
(bound at takeWhileVector.hs:69:1)
In the expression: (x :- takeWhileVector f xs)
In an equation for ‘takeWhileVector’:
takeWhileVector f (x :- xs) = (x :- takeWhileVector f xs)
``````

I would have thought that my type definition for takeWhileVector says the following:

For all types 'a' and 'n's of kind Nat, this function returns a 'Vector a m', where 'm' is kind Nat.

Do I need to change the type signature of takeWhileVector to be more specific so that it shows that the result is Vector a (m :: Nat)? Otherwise, how can I change this to have it compile?

The type you suggest can not be implemented, i.e. it is not inhabited:

``````takeWhileVector :: (a -> Bool) -> Vector a n -> Vector a m
``````

Remember that the caller chooses the type variables `a,n,m`. This means that the caller can use your function as e.g.

``````takeWhileVector :: (a -> Bool) -> Vector a Z -> Vector a (S Z)
``````

which is nonsense, since you can't produce some `a`s if you got none at the beginning. Even more practically, the caller of this function is not meant to be able to choose how many results to have and pass a completely unrelated function -- that would disagree with the intended semantics of `takeWhile`.

I guess what you really mean is something like

``````takeWhileVector :: (a -> Bool) -> Vector a n -> exists m. Vector a m
``````

except that `exists` is not valid Haskell syntax. Instead, you need something like

``````data SomeVector a where
S :: Vector a m -> SomeVector a

takeWhileVector :: (a -> Bool) -> Vector a n -> SomeVector a
``````

# Related:

## First three items of a list in Haskell

I am very new to Haskell, and struggling a bit with a function here. The premise is simple enough: Run through a list, and combine each 3 items next to each other with another function and return a list with the results. The problem is to do it in a...

## Thread blocked indefinitely in an MVar operation

I have been attempting to debug a problem when using multiple MVars, however to no luck. My code uses two MVars: one to store the servers current state, and another to pass network events to and from the client threads. However after connecting and disconnecting several times, the server stops...

## How to convert a Rational into a “pretty” String?

I want to display some Rational values in their decimal expansion. That is, instead of displaying 3 % 4, I would rather display 0.75. I'd like this function to be of type Int -> Rational -> String. The first Int is to specify the maximum number of decimal places, since...

## How does Frege generalize number literals?

It appears that Frege can evaluate 1/2 to return the Double value 0.5. The literal 1 is of type Int. It seems to be promoted to Double, which is a type in the Real class and thus knows the / operator. How does this happen? Is it using the Haskell...

I have been reading this StackOverflow post in which we are advised to use the haskellng package set. I have also read this but I did not understand what haskellng is. I have read this too, but I still don't know what haskellng is. Could someone please explain what haskellng...

## apply a transformation with function inline

Starting from a simple case of "fold" (I used (+) but can be anything else): Prelude.foldl (+) 0 [10,20,30] is it possible apply an inline transformation similar to (that doesn't work): Prelude.foldl ((+) . (\x -> read x :: Int)) 0 ["10","20","30"] In case not, is there an alternative to...

## Idiomatic list construction

I'm very new to Haskell and functional programming in general, so I don't really know how to make this code idiomatic: type Coord = Double data Point = Point Coord Coord Coord deriving Show type Polyline = [Point] -- Add a point to a polyline addPoint :: Polyline -> Point...

## Recursion scheme in Haskell for repeatedly breaking datatypes into “head” and “tail” and yielding a structure of results

In Haskell, I recently found the following function useful: listCase :: (a -> [a] -> b) -> [a] -> [b] listCase f [] = [] listCase f (x:xs) = f x xs : listCase f xs I used it to generate sliding windows of size 3 from a list, like...

## Combining Event and an attribute in threepenny-gui

I have an Event String which I want to sink into a textarea. This works fine, but now I want to combine the current value of a checkbox selection to this string. First I did this by using checkedChange of the checkbox which works, but has a problem. If the...

I would like to install this vim plugin: https://github.com/begriffs/haskell-vim-now When trying to run the suggested installation script: curl -o - https://raw.githubusercontent.com/begriffs/haskell-vim-now/master/install.sh | bash I get: --- Cabal version 1.18 or later is required. Aborting. I then try to install a newer version of cabal: [email protected]:~/Downloads/cabal-install-1.22.6.0\$ ./bootstrap.sh The response I get:...

## “conflicting implementations for trait” when trying to be generic

types,rust
Background: I'm using the nalgebra library and I want to create a structure that represents a multivariate normal distribution. M is the type of the matrix, e.g. Mat4<f64>. My current attempt looks like this: use std::ops::Mul; use std::marker::PhantomData; use nalgebra::*; #[allow(non_snake_case)] pub struct Multivarð©<N, V, M: SquareMat<N, V>> { μ:...

## Running executable files using Haskell

Say there's a C++ code that I've compiled into an executable using: g++ test.cpp -o testcpp I can run this using Terminal (I'm using OS X), and provide an input file for processing inside the C++ program, like: ./testcpp < input.txt I was wondering if doing this is possible, from...

## How do I avoid writing this type of Haskell boilerplate code

I run into this situation often enough for it to be annoying. Let's say I have a sum type which can hold an instance of x or a bunch of other things unrelated to x - data Foo x = X x | Y Int | Z String | ...(other...

## Hook into GHC runtime system

I have been looking at how transactional memory is implemented in Haskell, and I am not sure I understand how the STM operations exposed to the programmer hook into the runtime system functions written in C. In ghc/libraries/base/GHC/Conc/Sync.hs of the git repo, I see the following definitions: -- |A monad...

## why (int) ( 307.03 * 100) = 30702 [duplicate]

php,types,floating-point,int
This question already has an answer here: Is floating point math broken? 18 answers Today my coworker stumbled on this: \$s = floatval("307.03"); \$s = \$s * 100; echo intval(\$s); //30702 float value or round(\$s) return 30703 as expected. I guess it's a problem connected with float to int...

## Haskell return lazy string from file IO

Here I'm back again with a (for me) really strange behaviour of my newest masterpiece... This code should read a file, but it doesn't: readCsvContents :: String -> IO ( String ) readCsvContents fileName = do withFile fileName ReadMode (\handle -> do contents <- hGetContents handle return contents ) main...

I am trying to install the paradox theorem prover sourced from here. When I run the makefile this is the command that runs: ghc -optl -static -lstdc++ -I../instantiate -I../minisat/current-base ../minisat/current-base/Solver.or ../minisat/current-base/Prop.or ../instantiate/MiniSatWrapper.or ../instantiate/MiniSatInstantiateClause.or -fglasgow-exts -O2 -static -threaded -main-is Paradox.Main.main --make Paradox.Main -o paradox And it results in several errors like...

## Get each fibbonacci value in haskell

I'm learning haskell and I have the following code: fib a b = a : fib b (a + b) findFibSum = sum [x | x <- fib 1 2, mod x 2 == 0 && x < 100] If I run findFibSum nothing happens, it just sits there. Shouldn't...

## Refactor an IO recursive loop into a monad folding in Haskell

I writing a tcp server, and here's my main loop method: serverLoop :: Socket -> IO () serverLoop sock = do (conn, _) <- accept sock forkIO \$ handleConn conn serverLoop sock (Note: handleConn :: Socket -> IO () is a function specific to my program.) I would like to...

I wrote the following logical expression evaluator. It works for simple 2-member expressions, and it runs but produces a fault for expression containing other expressions as the second/first member. Here's my code. data Expression = Literal Bool | Operation Operator Expression Expression data Operator = AND | OR eval ::...

## Mapping with IO actions in Haskell

I have a function that takes two filenames, and reads the contents of those two files into Strings, and then returns if they match or not. Here's the function: f :: String -> String -> IO Bool f fileName1 fileName2 = do str1 <- readFile fileName1 str2 <- readFile fileName2...

## Why is f <\$> g <\$> x equivalent to (f . g) <\$> x although <\$> is not right-associative?

Why is f <\$> g <\$> x equivalent to (f . g) <\$> x although <\$> is not right-associative? (This kind of equivalence is valid in a popular idiom with plain \$, but currently \$ is right-associative!) <*> has the same associativity and precedence as <\$>, but behaves differently! Example:...

## Setting id and class with the haskell diagrams package

I am working with the diagrams package for haskell, and I am using the SVG backend. I embed the SVG markup directly into an HTML document, so that the graph as a part of a web page. I have built a pretty cool looking bar graph, and I would like...

## Why Comparison Of two Integer using == sometimes works and sometimes not? [duplicate]

java,types,comparison
This question already has an answer here: Why does 128==128 return false but 127==127 return true in this code? 4 answers Why equal operator works for Integer value until 128 number? [duplicate] 7 answers I know that i am comparing reference while i'm using == which is not a...

## Stopping condition on a recursive function - Haskell

So, I have this function which aims to align the text on the left without cutting words(only white spaces). However my problem is that I cannot find a stopping condition of the function and it goes infinitely. f n "" = "" --weak condition f n s = if n...

## Implementing map on a tree using fold

I am trying to implement a map using fold. I could do so in Haskell data Tree a = EmptyTree | Node a (Tree a) (Tree a) deriving (Show) foldTree :: Tree a -> b -> (b -> a -> b -> b) -> b foldTree EmptyTree d _ =...

## When will travis-ci support ghc 7.10?

I'd like to use travis-ci on my Haskell projects, but they require the latest version of GHC.

## C# - Get all types that been used in class A

c#,reflection,types
how can I get all the types that been used in specific type? Example for class "MyClass": [MyAttribute(new OtherType(TestEnum.EnumValue1))] public class MyClass:MyOtherClass { public Type MyType { get; set; } public string MyString { get; set; } private DateTime MyDateTime; [OtherAttribute()] public int MyMethod(double doubleNumber, float floatNumber) { justMyClass myJustClass...

## Why is lazy evaluation in Haskell “not being lazy”?

When I tried the following code in cghi: take 1 \$ take 1 \$ repeat [1..] I was expecting the result of 1 instead of [[1,2,3,4,5,6,7,8,9,10,... printing on my terminal. Why is lazy evaluation not functioning as I'm hoping under such situation?...

I'm using a graphic library in Haskell called ThreePennyUI. In this library the main function returns a UI monad object. This causes me much headache as when I attempt to unpack IO values into local variables I receive errors complaining of different monad types. Here's an example of my problem:...

## Haskell powerset function - How to avoid Couldn't match expected type `IO t0' with actual type `[[Integer]]'

I have a powerset implementation that I'm trying to run here: http://rextester.com/runcode. I'm still getting this error and can't figure out how to make it right. I'm trying to read as much as possible about IO in haskell but it is super hard for me. import Control.Monad (filterM) powerset =...

Haskell IO system is super hard to understand for me so i have question : How to read from standard input to list ? I know that there is function getLine :: IO String and interact. But i do not know how to convert the input to list so I...

## Fold over a heterogeneous, compile time, list

I have a list of heterogeneous types (or at least that's what I have in mind): data Nul data Bits b otherBits where BitsLst :: b -> otherBits -> Bits b otherBits NoMoreBits :: Bits b Nul Now, given an input type b, I want to go through all the...

## Unconstrained type parameters casting

c#,.net,types,casting
My situation: interface ISomeInterface { void DoSmth<T>(T other); } class Base : ISomeInterface { public virtual void DoSmth<T>(T other){ // for example do nothing } } class Derived<T2> : Base { Action<T2> MyAction {get;set;} public override void DoSmth<T>(T other){ if(typeof(T2).IsAssignableFrom(typeof(T))) MyAction((T2) other); } } This gives me an error: Cannot...

## Why doesn't `iterate` from the Prelude tie the knot?

Why isn't iterate defined like iterate :: (a -> a) -> a -> [a] iterate f x = xs where xs = x : map f xs in the Prelude?...

## Replace all [ ] with {} - as short as possible [on hold]

Given the code below: import Data.List; main = (readLn :: IO [Integer]) >>= print . subsequences It takes a list of integers from standard input (for example [1,2,3]) and outputs something like: [[],[1],[2],[1,2],[3],[1,3],[2,3],[1,2,3]] I want it to be like this: {},{1},{2},{1,2},{3},{1,3},{2,3},{1,2,3}} so my goal is to replace every [ and...

## Javadoc: Do parameter and return need an explicit type description

When Javadoc'ing, I don't know whether you should explicitly say whether the parameters are of type String or int. For example /** * This method does something * @param foo an object of type Foo * @param abc the number of doors, of type int * @return the number of...

## How to “wrap” monadic return value

I have the following code: data APNSIdentifier = NoIdentifier | Identifier Word32 deriving (Show, Eq) newtype APNSItem = Item Put createNotificationIdentifierItem :: APNSIdentifier -> APNSItem <--- here createNotificationIdentifierItem (Identifier identifier) = do putWord8 3 putWord16be 4 putWord32be identifier How can I "wrap" the Put monad with an APNSItem? Do I...

## SPARQL: How do I List and count each data type in an RDF dataset?

types,count,sparql
I am trying to count the instances of each datatype in a dataset. It is a simple dataset with only three data types: integer, string and dateTime. I can get the number of datatypes (3) by querying: SELECT (COUNT(DISTINCT datatype(?o)) AS ?dTypeCount) {?s ?p ?o. FILTER (isLiteral(?o)) } GROUP BY...

Consider the following IO code: ghci> let x = return 100 :: IO Int ghci> :t do { a <- x; print a; return 500 } do { a <- x; print a; return 500 } :: Num b => IO b My understanding of do notation/bind is that the...

I'm writing this small program basically to identify each input tokens as operator/parenthesis/int. However, I encountered a problem stating that Not in scope: data constructor `Integer' Here's what I have so far (Data.Char only defines isDigit, nothing else) import Data.Char (isDigit) data Token = TPlus | TTimes | TParenLeft |...

## Best practice for handling data types from 3rd party libraries in Haskell?

I'm just getting into my first real Haskell project of size (a web app), and I'm starting to run into issues with types from 3rd party libraries leaking all over my code. Here is a quick example: My Parser module imports Test.Parsec, and the exports a function (parseConfig) that returns...

## int* const* foo(int x); is a valid C function prototype. How do you “read” this return type?

c++,c,types,grammar
I notice that this is a valid prototype while reading through the ANSI C grammar spec from 1985 published by Jeff Lee and I compiled a function with this signature. What exactly might a function with this prototype return? What would a simple body of this function look like?

## Keep track of loop without a counter

Say, I got a list which length can be odd or even. Every iteration , I remove two items from the list. If there is one or no item at the end, I end the execution. If I store (length list)/2 every loop, I will get e.g. [5,4,3...] for a...

## Decremented value called in the recursion in Haskell

So, I have this function that aligns the text to the left for a given column width. I have already fixed some of its problems, but I am unable to make it not use the decremented parameter once it is called, but to return to the starting value of n....